| changeset 2950 | 0911cb7bf696 |
| parent 2561 | 7926f1cb45eb |
| child 3029 | 6fd3fc3254ee |
| 2949:adf22ee09738 | 2950:0911cb7bf696 |
|---|---|
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype trm = |
8 Vr "name" |
8 Vr "name" |
9 | Ap "trm" "trm" |
9 | Ap "trm" "trm" |
10 | Lm x::"name" t::"trm" bind (set) x in t |
10 | Lm x::"name" t::"trm" binds (set) x in t |
11 | Lt a::"lts" t::"trm" bind "bn a" in a t |
11 | Lt a::"lts" t::"trm" binds "bn a" in a t |
12 and lts = |
12 and lts = |
13 Lnil |
13 Lnil |
14 | Lcons "name" "trm" "lts" |
14 | Lcons "name" "trm" "lts" |
15 binder |
15 binder |
16 bn |
16 bn |