nominal2: TODO@c63ffe1735eb (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
2783 8412c7e503d4 misc Christian Urban <urbanc@in.tum.de> parents: 2719 diff changeset	4	- equations like
2719 dd5b60bccfd4 updated TODO Christian Urban <urbanc@in.tum.de> parents: 2452 diff changeset	5
2783 8412c7e503d4 misc Christian Urban <urbanc@in.tum.de> parents: 2719 diff changeset	6	\| "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
8412c7e503d4 misc Christian Urban <urbanc@in.tum.de> parents: 2719 diff changeset	7
8412c7e503d4 misc Christian Urban <urbanc@in.tum.de> parents: 2719 diff changeset	8	do not work
1555 73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	9
1987 72bed4519c86 Some of the exceptions that the parser should check in TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1808 diff changeset	10	Parser should check that:
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2383 diff changeset	11
1987 72bed4519c86 Some of the exceptions that the parser should check in TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1808 diff changeset	12	- 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	13	- 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	14	- bound arguments are not datatypes
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1987 diff changeset	15	- 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	16
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	Smaller things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1504 diff changeset	19	- maybe <type>_perm whould be called permute_<type>.simps;
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	that would conform with the terminology in Nominal2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2383 diff changeset	23	Other:
1808 d7a2c45b447a added TODO item about parser creating syntax for the wrong type Christian Urban <urbanc@in.tum.de> parents: 1802 diff changeset	24
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	- nested recursion, like types "trm list" in a constructor
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
1503 8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	27	- store information about defined nominal datatypes, so that
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	28	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	29

author	Christian Urban <urbanc@in.tum.de>
	Sun, 22 May 2011 10:20:18 +0200
changeset 2785	c63ffe1735eb
parent 2783	8412c7e503d4
child 2873	fac8b28f2a23
permissions	-rw-r--r--