From 7d602c10685c8b609ff9d2fabd46752e7ee4300c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Oct 2013 20:21:17 -0700 Subject: [PATCH] doc(todo): update todo Signed-off-by: Leonardo de Moura --- doc/todo.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/todo.md b/doc/todo.md index 62108bb413..ab07603cb1 100644 --- a/doc/todo.md +++ b/doc/todo.md @@ -3,7 +3,7 @@ To Do List - ~~Add `cast : Pi (A B : Type) (H : A = B) (a : A) : B`, and implement "casting propagation" in the type checker.~~ - ~~Modify the `let` construct to store the type of the value. The idea is to allow `let name : type := value in expr`. The type does not need to be provided by the user. However, the user may want to provide it as a hint for the Lean elaborator.~~ -- 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. +- ~~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: