| changeset 3132 | 87eca760dcba |
| parent 2686 | 52e1e98edb34 |
| child 3235 | 5ebd327ffb96 |
| 3131:3e37322465e2 | 3132:87eca760dcba |
|---|---|
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype lam = |
7 nominal_datatype lam = |
8 Var "name" |
8 Var "name" |
9 | App "lam" "lam" |
9 | App "lam" "lam" |
10 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
10 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
11 |
11 |
12 |
12 |
13 |
13 |
14 lemma alpha_test: |
14 lemma alpha_test: |
15 shows "Lam [x]. (Var x) = Lam [y]. (Var y)" |
15 shows "Lam [x]. (Var x) = Lam [y]. (Var y)" |