diff -r ab2aded5f7c9 -r 99583bd6a7b2 TODO --- a/TODO Mon Jun 20 09:59:18 2011 +0900 +++ b/TODO Mon Jun 20 10:16:12 2011 +0900 @@ -37,6 +37,9 @@ - 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: - nested recursion, like types "trm list" in a constructor