equal
deleted
inserted
replaced
17 |
17 |
18 - we also need to lift the size function for nominal |
18 - we also need to lift the size function for nominal |
19 datatypes |
19 datatypes |
20 |
20 |
21 Bigger things: |
21 Bigger things: |
|
22 |
|
23 - the alpha equivalence for |
|
24 |
|
25 Let as::assn t::trm bind "bn as" in t |
|
26 |
|
27 creates as premise |
|
28 |
|
29 EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t') |
|
30 |
|
31 but I think it should be |
|
32 |
|
33 as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t') |
|
34 |
|
35 (both are equivalent, but the second seems to be closer to |
|
36 the fv-function) |
22 |
37 |
23 - nested recursion, like types "trm list" in a constructor |
38 - nested recursion, like types "trm list" in a constructor |
24 |
39 |
25 - define permute_bn automatically and prove properties of it |
40 - define permute_bn automatically and prove properties of it |
26 |
41 |