equal
deleted
inserted
replaced
11 |
11 |
12 |
12 |
13 nominal_datatype foo: trm = |
13 nominal_datatype foo: trm = |
14 Var "name" |
14 Var "name" |
15 | App "trm" "trm" |
15 | App "trm" "trm" |
16 | Lam x::"name" t::"trm" bind x in t |
16 | Lam x::"name" t::"trm" binds x in t |
17 | Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2 |
17 | Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" binds "bn a1" in t1, binds "bn a2" in t2 |
18 | Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2 |
18 | Let2 x::"name" y::"name" t1::"trm" t2::"trm" binds x y in t1, binds y in t2 |
19 and assg = |
19 and assg = |
20 As_Nil |
20 As_Nil |
21 | As "name" x::"name" t::"trm" "assg" |
21 | As "name" x::"name" t::"trm" "assg" |
22 binder |
22 binder |
23 bn::"assg \<Rightarrow> atom list" |
23 bn::"assg \<Rightarrow> atom list" |