TODO.

TODO.md

@@ -23,10 +23,6 @@
   that would require multiple name transformations (i.e., composing multiple
   environment lookups).
 
-* Can `let0`, `let1`, and `letn` be simplified or combined? Do we really need
-  a `CLet` form that binds several names at once? Can the treatment of
-  unreachable type variables be simplified?
-
 * Can we remove the redundancy between `instance` and `instance_? (See next item.)
 
 * Introduce a combinator `ignore : 'a co -> unit co` that allows the solver to
@@ -37,6 +33,8 @@
   elaboration. Also, it could remove the need for a primitive `instance_`
   combinator, as `instance_ x ty` would correspond to `ignore (instance x ty)`.
 
+* Introduce a `forall` combinator so as to make it easy to express `∀α.c`.
+
 ## Error Handling
 
 * Attach exploitable information to the exception `VariableScopeEscape`.
@@ -62,12 +60,6 @@
   decoding is performed either during elaboration or after the
   unifier has encountered an error.
 
-* Improve the documentation produced by `make doc`.
-
-* Document the requirement that the function passed to `map` must be pure.
-  Use this hypothesis to remove the useless evaluation of `k1 env` in the
-  definition of `^^`.
-
 ## Test Suite
 
 * Improve the coverage of the test suite. Add explicit negative test cases.