equal
deleted
inserted
replaced
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype single_let: trm = |
7 nominal_datatype single_let: trm = |
8 Var "name" |
8 Var "name" |
9 | App "trm" "trm" |
9 | App "trm" "trm" |
10 | Lam x::"name" t::"trm" bind x in t |
10 | Lam x::"name" t::"trm" binds x in t |
11 | Let a::"assg" t::"trm" bind "bn a" in t |
11 | Let a::"assg" t::"trm" binds "bn a" in t |
12 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 |
12 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" binds (set) x in y t t1 t2 |
13 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
13 | Bar x::"name" y::"name" t::"trm" binds y x in t x y |
14 | Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 |
14 | Baz x::"name" t1::"trm" t2::"trm" binds (set) x in t1, binds (set+) x in t2 |
15 and assg = |
15 and assg = |
16 As "name" x::"name" t::"trm" bind x in t |
16 As "name" x::"name" t::"trm" binds x in t |
17 binder |
17 binder |
18 bn::"assg \<Rightarrow> atom list" |
18 bn::"assg \<Rightarrow> atom list" |
19 where |
19 where |
20 "bn (As x y t) = [atom x]" |
20 "bn (As x y t) = [atom x]" |
21 |
21 |