1 Function definitions |
1 Function definitions |
2 |
2 |
3 - export proofs bout alpha_bn |
3 - nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...? |
4 - equations like |
|
5 |
4 |
|
5 - nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt] |
|
6 |
|
7 - equations that talk about True/False, for example |
6 | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)" |
8 | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)" |
|
9 do not work (since 'function' does not work) |
7 |
10 |
8 do not work |
11 - equivariance for functions can be derived automatically (knowing termination and |
|
12 equivariance of the graph). |
9 |
13 |
10 Parser should check that: |
14 - for multiple simultanously defined functions, compatibility cases should fold the |
|
15 definition and derive eqvt_at for the folded one |
|
16 |
|
17 - equivariance of the graph for multiple functions does not use equivariance |
|
18 infrastructure |
|
19 |
|
20 Nominal_Datatype Parser should check that: |
11 |
21 |
12 - types of bindings match types of binding functions |
22 - types of bindings match types of binding functions |
13 - fsets are not bound in lst bindings |
23 - fsets are not bound in lst bindings |
14 - bound arguments are not datatypes |
24 - bound arguments are not datatypes |
15 - binder is referred to by name and not by type |
25 - binder is referred to by name and not by type |
16 |
26 |
17 Smaller things: |
27 Smaller things: |
18 |
28 |
19 - maybe <type>_perm whould be called permute_<type>.simps; |
29 - maybe <t1_t2>.perm_simps should be called permute_<type>.simps; |
20 that would conform with the terminology in Nominal2 |
30 that would conform with the terminology in Nominal2 |
21 |
31 |
22 |
32 |
23 Other: |
33 Other: |
24 |
34 |