equal
deleted
inserted
replaced
20 |
20 |
21 Bigger things: |
21 Bigger things: |
22 |
22 |
23 - nested recursion, like types "trm list" in a constructor |
23 - nested recursion, like types "trm list" in a constructor |
24 |
24 |
|
25 - define permute_bn automatically and prove properties of it |
|
26 |
|
27 - prove renaming-of-binders lemmas |
|
28 |
25 - strong induction rules |
29 - strong induction rules |
26 |
30 |
27 - check support equations for more bindings per constructor |
31 - check support equations for more bindings per constructor |
28 |
32 |
29 - automate the proofs that are currently proved with sorry: |
33 - For binding functions that call other binding functions |
30 alpha_equivp |
34 the following are proved with cheat_tac: |
|
35 bn_eqvt, bn_rsp, alpha_bn_rsp, constr_rsp |
31 |
36 |
32 - store information about defined nominal datatypes, so that |
37 - store information about defined nominal datatypes, so that |
33 it can be used to define new types that depend on these |
38 it can be used to define new types that depend on these |
34 |
|
35 - make parser aware of bn functions that call other bn functions |
|
36 and reflect it in the datastructure passed to Fv/Alpha generation |
|
37 |
39 |
38 - make parser aware of recursive and of different versions of abs |
40 - make parser aware of recursive and of different versions of abs |
39 |
41 |
40 Less important: |
42 Less important: |
41 |
43 |