equal
deleted
inserted
replaced
16 ANil | ACons var exp assn |
16 ANil | ACons var exp assn |
17 binder |
17 binder |
18 bn |
18 bn |
19 where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)" |
19 where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)" |
20 |
20 |
|
21 (* NEEDS FIXING |
21 nominal_datatype ('ann::fs) exp2 = |
22 nominal_datatype ('ann::fs) exp2 = |
22 Var var |
23 Var2 var |
23 | App "'ann exp2" var |
24 | App2 "'ann exp2" var |
24 | LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as |
25 | LetA2 as::"'ann assn2" body::"'ann exp2" binds "bn2 as" in body as |
25 | Lam x::var body::"'ann exp2" binds x in body |
26 | Lam2 x::var body::"'ann exp2" binds x in body |
26 and ('ann::fs) assn2 = |
27 and ('ann::fs) assn2 = |
27 ANil |
28 ANil2 |
28 | ACons var "'ann exp2" 'ann "'ann assn2" |
29 | ACons2 var "'ann exp2" 'ann "'ann assn2" |
29 binder |
30 binder |
30 bnn :: "('ann::fs) assn2 \<Rightarrow> atom list" |
31 bn2 :: "('ann::fs) assn2 \<Rightarrow> atom list" |
31 where |
32 where |
32 "bnn ANil = []" |
33 "bn2 ANil2 = []" |
33 | "bnn (ACons x a t as) = (atom x) # (bnn as)" |
34 | "bn2 (ACons2 x a t as) = (atom x) # (bn2 as)" |
34 |
35 *) |
35 |
36 |
36 (* a nominal datatype with type variables and sorts *) |
37 (* a nominal datatype with type variables and sorts *) |
37 |
38 |
38 |
39 |
39 (* the sort constraints need to be attached to the *) |
40 (* the sort constraints need to be attached to the *) |
47 |
48 |
48 instance nat :: s1 .. |
49 instance nat :: s1 .. |
49 instance int :: s2 .. |
50 instance int :: s2 .. |
50 |
51 |
51 nominal_datatype ('a::s1, 'b::s2, 'c::at) lam = |
52 nominal_datatype ('a::s1, 'b::s2, 'c::at) lam = |
52 Var "name" |
53 Var3 "name" |
53 | App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam" |
54 | App3 "('a, 'b, 'c) lam" "('a, 'b, 'c) lam" |
54 | Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l |
55 | Lam3 x::"name" l::"('a, 'b, 'c) lam" binds x in l |
55 | Foo "'a" "'b" |
56 | Foo3 "'a" "'b" |
56 | Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *) |
57 | Bar3 x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *) |
57 |
58 |
58 term Foo |
59 term Foo |
59 term Bar |
60 term Bar |
60 |
61 |
61 thm lam.supp lam.fresh |
62 thm lam.supp lam.fresh |