michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(todo): update todo list

Browse source
This commit is contained in:
Leonardo de Moura 2013-11-07 15:24:41 -08:00
parent 9c18439eb2
commit a16c41c2c7
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
doc/todo.md
View file

@ -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).~~ - ~~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`.~~ - ~~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 design our own configuration language.~~
~~- We use an off-the-shelf embedded language such as [Lua](http://www.lua.org).~~ - ~~We use an off-the-shelf embedded language such as [Lua](http://www.lua.org).~~
~~- We use Lean itself.~~ - ~~We use Lean itself.~~
- Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.
- ~~Higher-Order unification and matching~~. - ~~Higher-Order unification and matching~~.
- Rewriter (and Rewriter Combinators). - Rewriter (and Rewriter Combinators).