equal
deleted
inserted
replaced
33 Bigger things: |
33 Bigger things: |
34 |
34 |
35 - Parser adds syntax for raw datatype, but should |
35 - Parser adds syntax for raw datatype, but should |
36 add for lifted datatype. |
36 add for lifted datatype. |
37 |
37 |
38 - the alpha equivalence for |
|
39 |
|
40 Let as::assn t::trm bind "bn as" in t |
|
41 |
|
42 creates as premise |
|
43 |
|
44 EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t') |
|
45 |
|
46 but I think it should be |
|
47 |
|
48 as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t') |
|
49 |
|
50 (both are equivalent, but the second seems to be closer to |
|
51 the fv-function) |
|
52 |
|
53 - when there are more than one shallow binder, then alpha |
|
54 equivalence creates more than one permutation. According |
|
55 to the paper, this is incorrect. |
|
56 |
|
57 Example in Classical.thy. |
|
58 |
|
59 - check whether weirdo example in TestMorePerm works |
|
60 with shallow binders |
|
61 |
|
62 - nested recursion, like types "trm list" in a constructor |
38 - nested recursion, like types "trm list" in a constructor |
63 |
39 |
64 - define permute_bn automatically and prove properties of it |
40 - define permute_bn automatically and prove properties of it |
65 |
41 |
66 - prove renaming-of-binders lemmas |
42 - prove renaming-of-binders lemmas |