nominal2: TODO@8639077e0f43 (annotated)

1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	Smaller things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	- case names for "weak" induction rules (names of the
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	constructors); see page 61/62 and 170 in Tutorial
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	- <type>_perm rules should be added to the simplifier;
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	maybe <type>_perm whould be called permute_<type>.simps;
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	that would conform with the terminology in Nominal2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	- <type>_fv / <type>_bn / <type>_distinct should also be
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	added to the simplifier
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
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	Bigger things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	- nested recursion, like types "trm list" in a constructor
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	- strong induction rules
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
1502 cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	20	- show support equations
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
1502 cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	22	- automate the proofs that are currently proved with sorry:
cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	23	alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
1503 8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	24
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
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	28	- make 3 versions of Abs
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	29
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	30	- make parser aware of recursive and of different versions of abs

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Thu, 18 Mar 2010 10:15:57 +0100
changeset 1503	8639077e0f43
parent 1502	cc0dcf248da3
child 1504	f685be70a464
permissions	-rw-r--r--