diff --git a/doc/todo.md b/doc/todo.md index ff910dc83e..79c2441573 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -7,9 +7,9 @@ To Do List - ~~Reconsider whether meta-variables should be in `expr` or not. Metavariables (aka holes) are fundamental in our [design](design.md).~~ - ~~Improve Lean pretty printer for Pi's. For example, it produces `Var a : Pi (A : Type) (_ : A), A` instead of `Var a : Pi (A : Type), A -> A`.~~ - ~~ Decide what will be the main technique for customizing Lean's behavior. The elaborator manager will have many building blocks that can be put together in many different ways. Possible solutions:~~ - ~~- We design our own configuration language.~~ - ~~- We use an off-the-shelf embedded language such as [Lua](http://www.lua.org).~~ - ~~- We use Lean itself.~~ + - ~~We design our own configuration language.~~ + - ~~We use an off-the-shelf embedded language such as [Lua](http://www.lua.org).~~ + - ~~We use Lean itself.~~ - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. - ~~Higher-Order unification and matching~~. - Rewriter (and Rewriter Combinators).