From 30d54fa483d3cba62b893d09dcf82e2ee2f03640 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Nov 2013 15:25:03 -0800 Subject: [PATCH] chore(todo): update todo list --- doc/todo.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/todo.md b/doc/todo.md index 79c244157..db6391017 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -6,7 +6,7 @@ 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:~~ +- ~~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.~~