nominal2: TODO@e6bf6790da7d (annotated)

2719 dd5b60bccfd4 updated TODO Christian Urban <urbanc@in.tum.de> parents: 2452 diff changeset	1	Function definitions
dd5b60bccfd4 updated TODO Christian Urban <urbanc@in.tum.de> parents: 2452 diff changeset	2
dd5b60bccfd4 updated TODO Christian Urban <urbanc@in.tum.de> parents: 2452 diff changeset	3	- export proofs bout alpha_bn
dd5b60bccfd4 updated TODO Christian Urban <urbanc@in.tum.de> parents: 2452 diff changeset	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 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2383 diff changeset	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 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	Smaller things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	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 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	that would conform with the terminology in Nominal2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2383 diff changeset	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 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	- nested recursion, like types "trm list" in a constructor
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
1503 8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	23	- store information about defined nominal datatypes, so that
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	24	it can be used to define new types that depend on these
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	25

author	Christian Urban <urbanc@in.tum.de>
	Wed, 16 Feb 2011 14:03:26 +0000
changeset 2724	e6bf6790da7d
parent 2719	dd5b60bccfd4
child 2783	8412c7e503d4
permissions	-rw-r--r--