chore(todo): update todo list
This commit is contained in:
parent
57b9657bf0
commit
9c18439eb2
1 changed files with 4 additions and 4 deletions
|
@ -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).
|
||||
|
|
Loading…
Reference in a new issue