equal
deleted
inserted
replaced
129 \<close> |
129 \<close> |
130 |
130 |
131 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i" |
131 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i" |
132 where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)" |
132 where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)" |
133 |
133 |
134 definition nil :: "i" (\<open>([])\<close>) |
134 definition nil :: "i" (\<open>[]\<close>) |
135 where "[] == inl(one)" |
135 where "[] == inl(one)" |
136 |
136 |
137 definition cons :: "[i,i]\<Rightarrow>i" (infixr \<open>$\<close> 80) |
137 definition cons :: "[i,i]\<Rightarrow>i" (infixr \<open>$\<close> 80) |
138 where "h$t == inr(<h,t>)" |
138 where "h$t == inr(<h,t>)" |
139 |
139 |