TODO.

TODO

@@ -12,6 +12,14 @@ demos/system-F-type:
 demos/system F-type-term:
   deal with both kinds of variables. (One or two namespaces?)
 
+Implement an alpha-respecting comparison, following Unbound.
+  Just convert to locally nameless on the fly, followed with
+  a lexicographic comparison.
+
+Simultaneous unbinding.
+
+LFresh monad. (Locally fresh names, for better printing.)
+
 Implement fused copy/subst, fused avoid/subst?
   Implement a kit that composes two kits, so as to easily implement fused operations.
   Composition of classes? Or composition of kit objects? ...
@@ -37,6 +45,7 @@ Deal with more complex forms of binding.
   e.g., or-patterns, join-calculus
   let, let rec, multiple let, multiple let rec, telescopes
   What about the distinction between expression types and pattern types?
+  Term mode versus pattern mode in Unbound.
 
 Try dealing with binding and hash-consing at the same time.