| changeset 2950 | 0911cb7bf696 |
| parent 2645 | 09cf78bb53d4 |
| child 3071 | 11f6a561eb4b |
| child 3190 | 1b7c034c9e9e |
| 2949:adf22ee09738 | 2950:0911cb7bf696 |
|---|---|
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 nominal_datatype lam = |
9 nominal_datatype lam = |
10 Var "name" |
10 Var "name" |
11 | App "lam" "lam" |
11 | App "lam" "lam" |
12 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100,100] 100) |
12 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100,100] 100) |
13 |
13 |
14 text {* Typing *} |
14 text {* Typing *} |
15 |
15 |
16 nominal_datatype ty = |
16 nominal_datatype ty = |
17 TVar string |
17 TVar string |