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

doc(todo): update todo.md

Browse source
This commit is contained in:
Leonardo de Moura 2013-10-02 09:37:53 -07:00
parent 5bd6ba37d0
commit e01da4d4e5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/todo.md
View file

@ -11,7 +11,7 @@ To Do List
- 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).
- [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework. - [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework.
- Implement independent type checker using a different programming language (e.g., OCaml). - Implement independent type checker using a different programming language (e.g., OCaml).