--- a/TODO	Mon Jun 20 20:09:30 2011 +0900
+++ b/TODO	Mon Jun 20 20:09:51 2011 +0900
@@ -1,13 +1,23 @@
 Function definitions
 
-- export proofs bout alpha_bn
-- equations like
+- nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?
 
+- nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]
+
+- equations that talk about True/False, for example
     | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
+  do not work (since 'function' does not work)
 
-  do not work
+- equivariance for functions can be derived automatically (knowing termination and
+  equivariance of the graph).
 
-Parser should check that:
+- for multiple simultanously defined functions, compatibility cases should fold the
+  definition and derive eqvt_at for the folded one
+
+- equivariance of the graph for multiple functions does not use equivariance
+  infrastructure
+
+Nominal_Datatype Parser should check that:
 
 - types of bindings match types of binding functions
 - fsets are not bound in lst bindings
@@ -16,9 +26,19 @@
 
 Smaller things:
 
-- maybe <type>_perm whould be called permute_<type>.simps;
+- maybe <t1_t2>.perm_simps should be called permute_<type>.simps;
   that would conform with the terminology in Nominal2
 
+- nominal_induct does not work without an induction rule
+
+- nominal_induct throws strange "THM" exceptions if not enough
+  variables are given
+
+- nominal_induct cannot avoid a term (for example function applied
+  to an argument).
+
+- .induct and .exhaust could be the default methods for induction/cases
+  on nominal datatypes
 
 Other: