2719
|
1 |
Function definitions
|
|
2 |
|
|
3 |
- export proofs bout alpha_bn
|
|
4 |
|
1555
|
5 |
|
1987
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
6 |
Parser should check that:
|
2452
|
7 |
|
1987
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
8 |
- 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
|
9 |
- 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
|
10 |
- bound arguments are not datatypes
|
2045
|
11 |
- 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
|
12 |
|
1501
|
13 |
Smaller things:
|
|
14 |
|
1510
|
15 |
- maybe <type>_perm whould be called permute_<type>.simps;
|
1501
|
16 |
that would conform with the terminology in Nominal2
|
|
17 |
|
|
18 |
|
2452
|
19 |
Other:
|
1808
d7a2c45b447a
added TODO item about parser creating syntax for the wrong type
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
|
1501
|
21 |
- nested recursion, like types "trm list" in a constructor
|
|
22 |
|
1503
|
23 |
- store information about defined nominal datatypes, so that
|
|
24 |
it can be used to define new types that depend on these
|
|
25 |
|