equal
deleted
inserted
replaced
263 | PS "name" |
263 | PS "name" |
264 | PD "name \<times> name" |
264 | PD "name \<times> name" |
265 binder |
265 binder |
266 f::"pat \<Rightarrow> name set" |
266 f::"pat \<Rightarrow> name set" |
267 where |
267 where |
268 "f PN = {}" |
268 "f PN = ({} :: name set)" |
269 | "f (PS x) = {x}" |
269 | "f (PS x) = {x}" |
270 | "f (PD (x,y)) = {x,y}" |
270 | "f (PD (x,y)) = {x,y}" |
271 |
271 |
272 nominal_datatype trm2 = |
272 nominal_datatype trm2 = |
273 Var2 "name" |
273 Var2 "name" |
279 | PS2 "name" |
279 | PS2 "name" |
280 | PD2 "pat2 \<times> pat2" |
280 | PD2 "pat2 \<times> pat2" |
281 binder |
281 binder |
282 f2::"pat2 \<Rightarrow> name set" |
282 f2::"pat2 \<Rightarrow> name set" |
283 where |
283 where |
284 "f2 PN2 = {}" |
284 "f2 PN2 = ({} :: name set)" |
285 | "f2 (PS2 x) = {x}" |
285 | "f2 (PS2 x) = {x}" |
286 | "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)" |
286 | "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2 :: name set)" |
287 |
287 |
288 text {* example type schemes *} |
288 text {* example type schemes *} |
289 datatype ty = |
289 datatype ty = |
290 Var "name" |
290 Var "name" |
291 | Fun "ty" "ty" |
291 | Fun "ty" "ty" |