| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 04 Feb 2011 04:45:04 +0000 | |
| changeset 2719 | dd5b60bccfd4 |
| parent 2452 | 39f8d405d7a2 |
| child 2783 | 8412c7e503d4 |
| permissions | -rw-r--r-- |
| 2719 | 1 |
Function definitions |
2 |
||
3 |
- export proofs bout alpha_bn |
|
4 |
||
|
1555
73992021c8f0
Described automatically created funs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1527
diff
changeset
|
5 |
|
|
1987
72bed4519c86
Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1808
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>
parents:
1808
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>
parents:
1808
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>
parents:
1808
diff
changeset
|
10 |
- bound arguments are not datatypes |
|
2045
6800fcaafa2a
Separate Term8, as it may work soon.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1987
diff
changeset
|
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>
parents:
1808
diff
changeset
|
12 |
|
| 1501 | 13 |
Smaller things: |
14 |
||
|
1510
be911e869fde
Added fv,bn,distinct,perm to the simplifier.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1504
diff
changeset
|
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>
parents:
1802
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 |