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

doc(todo): update todo list

Browse source
This commit is contained in:
Leonardo de Moura 2014-02-08 09:23:13 -08:00
parent 1f3e0f7a38
commit ded72f94b2
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/todo.md
View file

@ -14,4 +14,6 @@ To Do List
- Independent type checker using a different programming language (e.g., F* or OCaml). - Independent type checker using a different programming language (e.g., F* or OCaml).
- Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs. - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.
- Re-implement apply-tactic. - Re-implement apply-tactic.
- Improve performance of `is_convertible` and `is_definitionally_equal` predicates - Improve performance of `is_convertible` and `is_definitionally_equal` predicates.
- Create notation sets. We are currently all notation in a "single bag".
- Improve macro support, and allow users to provide arbitrary parser extensions using Lua.