equal
deleted
inserted
replaced
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 nominal_datatype exp = |
9 nominal_datatype exp = |
10 Var "name" |
10 Var "name" |
11 | App "exp" "exp" |
11 | App "exp" "exp" |
12 | Lam x::"name" e::"exp" bind x in e |
12 | Lam x::"name" e::"exp" binds x in e |
13 | Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1 |
13 | Let x::"name" p::"pat" e1::"exp" e2::"exp" binds (set) x in e2, binds (set) "bp p" in e1 |
14 and pat = |
14 and pat = |
15 PVar "name" |
15 PVar "name" |
16 | PUnit |
16 | PUnit |
17 | PPair "pat" "pat" |
17 | PPair "pat" "pat" |
18 binder |
18 binder |