| changeset 2950 | 0911cb7bf696 |
| parent 2936 | a6acbb20fbca |
| child 2956 | 7e1c309bf820 |
| 2949:adf22ee09738 | 2950:0911cb7bf696 |
|---|---|
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype 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 as::"assn" t::"trm" bind "bn as" in t |
11 | Let as::"assn" t::"trm" binds "bn as" in t |
12 and assn = |
12 and assn = |
13 ANil |
13 ANil |
14 | ACons "name" "trm" "assn" |
14 | ACons "name" "trm" "assn" |
15 binder |
15 binder |
16 bn |
16 bn |