From 9c18439eb238769a4ccccc9701f4206ca9a3893d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Nov 2013 15:24:09 -0800 Subject: [PATCH] chore(todo): update todo list --- doc/todo.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/todo.md b/doc/todo.md index ab07603cb..ff910dc83 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -6,10 +6,10 @@ To Do List - ~~Refactor the elaborator code. The elaborator will be one of the main data-structures in Lean. The elaborator manager should be shared between different frontends.~~ - ~~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. +- ~~ 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.~~ - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. - ~~Higher-Order unification and matching~~. - Rewriter (and Rewriter Combinators).