| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Thu, 18 Mar 2010 23:20:46 +0100 | |
| changeset 1526 | 770a66131bd3 |
| parent 1516 | e3a82a3529ce |
| child 1527 | e1c74b864b1b |
| permissions | -rw-r--r-- |
| 1501 | 1 |
Smaller things: |
2 |
||
|
1510
be911e869fde
Added fv,bn,distinct,perm to the simplifier.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1504
diff
changeset
|
3 |
- maybe <type>_perm whould be called permute_<type>.simps; |
| 1501 | 4 |
that would conform with the terminology in Nominal2 |
5 |
||
6 |
||
7 |
Bigger things: |
|
8 |
||
9 |
- nested recursion, like types "trm list" in a constructor |
|
10 |
||
11 |
- strong induction rules |
|
12 |
||
|
1502
cc0dcf248da3
Which proofs need a 'sorry'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1501
diff
changeset
|
13 |
- show support equations |
| 1501 | 14 |
|
|
1502
cc0dcf248da3
Which proofs need a 'sorry'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1501
diff
changeset
|
15 |
- automate the proofs that are currently proved with sorry: |
|
cc0dcf248da3
Which proofs need a 'sorry'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1501
diff
changeset
|
16 |
alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp |
| 1503 | 17 |
|
18 |
- store information about defined nominal datatypes, so that |
|
19 |
it can be used to define new types that depend on these |
|
20 |
||
21 |
- make 3 versions of Abs |
|
22 |
||
|
1504
f685be70a464
fv_bn may need to call other fv_bns.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1503
diff
changeset
|
23 |
- make parser aware of bn functions that call other bn functions |
|
f685be70a464
fv_bn may need to call other fv_bns.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1503
diff
changeset
|
24 |
and reflect it in the datastructure passed to Fv/Alpha generation |
|
f685be70a464
fv_bn may need to call other fv_bns.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1503
diff
changeset
|
25 |
|
| 1503 | 26 |
- make parser aware of recursive and of different versions of abs |