Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update TODO
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 25 Mar 2010 15:06:58 +0100
changeset 1649 ba837d3ed37f
parent 1648 1ca332adc247
child 1650 4b949985cf57
Update TODO
TODO file | annotate | diff | comparison | revisions 
--- a/TODO	Thu Mar 25 14:31:51 2010 +0100
+++ b/TODO	Thu Mar 25 15:06:58 2010 +0100
@@ -22,19 +22,21 @@
 
 - nested recursion, like types "trm list" in a constructor
 
+- define permute_bn automatically and prove properties of it
+
+- prove renaming-of-binders lemmas
+
 - strong induction rules
 
 - check support equations for more bindings per constructor
 
-- automate the proofs that are currently proved with sorry:
-  alpha_equivp
+- For binding functions that call other binding functions
+  the following are proved with cheat_tac:
+    bn_eqvt, bn_rsp, alpha_bn_rsp, constr_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these
 
-- make parser aware of bn functions that call other bn functions
-  and reflect it in the datastructure passed to Fv/Alpha generation
-
 - make parser aware of recursive and of different versions of abs
 
 Less important:
nominal2