1501
|
1 |
Smaller things:
|
|
2 |
|
1510
|
3 |
- maybe <type>_perm whould be called permute_<type>.simps;
|
1501
|
4 |
that would conform with the terminology in Nominal2
|
|
5 |
|
1527
|
6 |
- we also need to lift the size function for nominal
|
|
7 |
datatypes
|
1501
|
8 |
|
|
9 |
Bigger things:
|
|
10 |
|
|
11 |
- nested recursion, like types "trm list" in a constructor
|
|
12 |
|
|
13 |
- strong induction rules
|
|
14 |
|
1502
|
15 |
- show support equations
|
1501
|
16 |
|
1502
|
17 |
- automate the proofs that are currently proved with sorry:
|
|
18 |
alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
|
1503
|
19 |
|
|
20 |
- store information about defined nominal datatypes, so that
|
|
21 |
it can be used to define new types that depend on these
|
|
22 |
|
|
23 |
- make 3 versions of Abs
|
|
24 |
|
1504
|
25 |
- make parser aware of bn functions that call other bn functions
|
|
26 |
and reflect it in the datastructure passed to Fv/Alpha generation
|
|
27 |
|
1503
|
28 |
- make parser aware of recursive and of different versions of abs
|