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

Update todo.md

Browse source
This commit is contained in:
Leonardo de Moura 2013-09-14 23:07:40 -07:00
parent a66d4ec42a
commit f527b931d8
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

@ -13,7 +13,7 @@ To Do List
- 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 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).
- Add `match` construct in `expr`. - Add `match` construct in `expr`.
- Add inductive datatype (families) in the environment. It will be a new kind of object. - Add inductive datatype (families) in the environment. It will be a new kind of object.