2719
|
1 |
Function definitions
|
|
2 |
|
2873
|
3 |
- nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?
|
2719
|
4 |
|
2873
|
5 |
- nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]
|
|
6 |
|
|
7 |
- equations that talk about True/False, for example
|
2783
|
8 |
| "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
|
2873
|
9 |
do not work (since 'function' does not work)
|
2783
|
10 |
|
2873
|
11 |
- equivariance for functions can be derived automatically (knowing termination and
|
|
12 |
equivariance of the graph).
|
1555
|
13 |
|
2873
|
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:
|
2452
|
21 |
|
1987
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
22 |
- types of bindings match types of binding functions
|
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
23 |
- fsets are not bound in lst bindings
|
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
24 |
- bound arguments are not datatypes
|
2045
|
25 |
- binder is referred to by name and not by type
|
1987
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
26 |
|
1501
|
27 |
Smaller things:
|
|
28 |
|
2873
|
29 |
- maybe <t1_t2>.perm_simps should be called permute_<type>.simps;
|
1501
|
30 |
that would conform with the terminology in Nominal2
|
|
31 |
|
2874
|
32 |
- nominal_induct does not work without an induction rule
|
|
33 |
|
|
34 |
- nominal_induct throws strange "THM" exceptions if not enough
|
|
35 |
variables are given
|
|
36 |
|
|
37 |
- nominal_induct cannot avoid a term (for example function applied
|
|
38 |
to an argument).
|
1501
|
39 |
|
2876
|
40 |
- .induct and .exhaust could be the default methods for induction/cases
|
|
41 |
on nominal datatypes
|
|
42 |
|
2452
|
43 |
Other:
|
1808
d7a2c45b447a
added TODO item about parser creating syntax for the wrong type
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
|
1501
|
45 |
- nested recursion, like types "trm list" in a constructor
|
|
46 |
|
1503
|
47 |
- store information about defined nominal datatypes, so that
|
|
48 |
it can be used to define new types that depend on these
|
|
49 |
|