nominal2: TODO@93a73eabbffc (annotated)

1555 73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	1
1987 72bed4519c86 Some of the exceptions that the parser should check in TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1808 diff changeset	2	Parser should check that:
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2383 diff changeset	3
1987 72bed4519c86 Some of the exceptions that the parser should check in TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1808 diff changeset	4	- 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	5	- 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	6	- bound arguments are not datatypes
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1987 diff changeset	7	- 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	8
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	Smaller things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1504 diff changeset	11	- maybe <type>_perm whould be called permute_<type>.simps;
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	that would conform with the terminology in Nominal2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2383 diff changeset	15	Other:
1808 d7a2c45b447a added TODO item about parser creating syntax for the wrong type Christian Urban <urbanc@in.tum.de> parents: 1802 diff changeset	16
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	- nested recursion, like types "trm list" in a constructor
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
1649 ba837d3ed37f Update TODO Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1576 diff changeset	19	- define permute_bn automatically and prove properties of it
ba837d3ed37f Update TODO Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1576 diff changeset	20
ba837d3ed37f Update TODO Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1576 diff changeset	21	- prove renaming-of-binders lemmas
ba837d3ed37f Update TODO Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1576 diff changeset	22
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	- strong induction rules
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
1503 8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	25	- store information about defined nominal datatypes, so that
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	26	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	27

author	Christian Urban <urbanc@in.tum.de>
	Tue, 28 Sep 2010 08:21:47 -0400
changeset 2495	93a73eabbffc
parent 2452	39f8d405d7a2
child 2719	dd5b60bccfd4
permissions	-rw-r--r--