equal
deleted
inserted
replaced
15 class s2 |
15 class s2 |
16 |
16 |
17 instance nat :: s1 .. |
17 instance nat :: s1 .. |
18 instance int :: s2 .. |
18 instance int :: s2 .. |
19 |
19 |
20 nominal_datatype ('a::"{s1,fs}", 'b::"{s2,fs}", 'c::at) lam = |
20 nominal_datatype ('a::s1, 'b::s2, 'c::at) lam = |
21 Var "name" |
21 Var "name" |
22 | App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam" |
22 | App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam" |
23 | Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l |
23 | Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l |
24 | Foo "'a" "'b" |
24 | Foo "'a" "'b" |
25 | Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *) |
25 | Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *) |
39 thm lam.size_eqvt |
39 thm lam.size_eqvt |
40 |
40 |
41 |
41 |
42 nominal_datatype ('alpha, 'beta, 'gamma) psi = |
42 nominal_datatype ('alpha, 'beta, 'gamma) psi = |
43 PsiNil |
43 PsiNil |
44 | Output "'alpha::fs" "'alpha::fs" "('alpha::fs, 'beta::fs, 'gamma::fs) psi" |
44 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" |
45 |
45 |
46 |
46 |
47 nominal_datatype 'a foo = |
47 nominal_datatype 'a foo = |
48 Node x::"name" f::"('a::fs) foo" binds x in f |
48 Node x::"name" f::"'a foo" binds x in f |
49 | Leaf "'a" |
49 | Leaf "'a" |
50 |
50 |
51 term "Leaf" |
51 term "Leaf" |
52 |
52 |
53 |
53 |