Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Issue with 'default'
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 08 Jun 2011 21:32:35 +0900
changeset 2836 1233af5cea95
parent 2835 80bbb0234025
child 2837 c78c2d565e99
Issue with 'default'
Nominal/Ex/TypeSchemes.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 12:30:56 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 21:32:35 2011 +0900
@@ -71,9 +71,12 @@
 using assms
 by blast
 
+--"The following two terms have the same type, however the first one is a valid default, but the second one no"
 definition "MYUNDEFINED \<equiv> undefined"
+term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys"
+term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). sum_case (\<lambda>x. Inl (undefined :: ty)) (\<lambda>x. Inr (undefined :: tys)) x"
 
-nominal_primrec (default "\<lambda>x. MYUNDEFINED")
+nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where
nominal2