equal
deleted
inserted
replaced
5 (* example 8 *) |
5 (* example 8 *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* this should work but gives an error at the moment: |
9 (* this should work but gives an error at the moment: |
10 seems like in the symmetry proof |
10 in alpha_bn_rsp proof. |
11 *) |
11 *) |
12 |
12 |
13 nominal_datatype foo = |
13 nominal_datatype foo = |
14 Foo0 "name" |
14 Foo0 "name" |
15 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
15 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
16 and bar = |
16 and bar = |
17 Bar0 "name" |
17 Bar0 "name" |
18 | Bar1 "name" s::"name" b::"bar" bind s in b |
18 | Bar1 "name" s::"name" b::"bar" bind_set s in b |
19 binder |
19 binder |
20 bv |
20 bv |
21 where |
21 where |
22 "bv (Bar0 x) = {}" |
22 "bv (Bar0 x) = {}" |
23 | "bv (Bar1 v x b) = {atom v}" |
23 | "bv (Bar1 v x b) = {atom v}" |