equal
deleted
inserted
replaced
|
1 Function definitions |
|
2 |
|
3 - export proofs bout alpha_bn |
|
4 |
1 |
5 |
2 Parser should check that: |
6 Parser should check that: |
3 |
7 |
4 - types of bindings match types of binding functions |
8 - types of bindings match types of binding functions |
5 - fsets are not bound in lst bindings |
9 - fsets are not bound in lst bindings |
14 |
18 |
15 Other: |
19 Other: |
16 |
20 |
17 - nested recursion, like types "trm list" in a constructor |
21 - nested recursion, like types "trm list" in a constructor |
18 |
22 |
19 - define permute_bn automatically and prove properties of it |
|
20 |
|
21 - prove renaming-of-binders lemmas |
|
22 |
|
23 - strong induction rules |
|
24 |
|
25 - store information about defined nominal datatypes, so that |
23 - store information about defined nominal datatypes, so that |
26 it can be used to define new types that depend on these |
24 it can be used to define new types that depend on these |
27 |
25 |