| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Thu, 18 Mar 2010 12:09:59 +0100 | |
| changeset 1510 | be911e869fde |
| parent 1504 | f685be70a464 |
| child 1516 | e3a82a3529ce |
| permissions | -rw-r--r-- |
| 1501 | 1 |
Smaller things: |
2 |
||
3 |
- case names for "weak" induction rules (names of the |
|
4 |
constructors); see page 61/62 and 170 in Tutorial |
|
5 |
||
|
1510
be911e869fde
Added fv,bn,distinct,perm to the simplifier.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1504
diff
changeset
|
6 |
- maybe <type>_perm whould be called permute_<type>.simps; |
| 1501 | 7 |
that would conform with the terminology in Nominal2 |
8 |
||
9 |
||
10 |
Bigger things: |
|
11 |
||
12 |
- nested recursion, like types "trm list" in a constructor |
|
13 |
||
14 |
- strong induction rules |
|
15 |
||
|
1502
cc0dcf248da3
Which proofs need a 'sorry'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1501
diff
changeset
|
16 |
- show support equations |
| 1501 | 17 |
|
|
1502
cc0dcf248da3
Which proofs need a 'sorry'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1501
diff
changeset
|
18 |
- 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
|
19 |
alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp |
| 1503 | 20 |
|
21 |
- store information about defined nominal datatypes, so that |
|
22 |
it can be used to define new types that depend on these |
|
23 |
||
24 |
- make 3 versions of Abs |
|
25 |
||
|
1504
f685be70a464
fv_bn may need to call other fv_bns.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1503
diff
changeset
|
26 |
- 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
|
27 |
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
|
28 |
|
| 1503 | 29 |
- make parser aware of recursive and of different versions of abs |