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-06 17:01:30 -08:00
parent e4579b93e4
commit 45ef10e2c1
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
doc/todo.md
View file

@ -1,9 +1,17 @@
To Do List To Do List
---------- ----------
- Add Sigma-types. - Add heterogeneous equality back into the kernel.
- Define natural numbers, lists, inductive datatypes from first principles. The goal is to use the HOL/Isabelle approach. - Finish Sigma-type support.
- Build Nat and List theories.
- Fix usability issues identified when formalizing optional and sum types.
- Add unification hints support in the Lean front-end.
- Improve simp tactic interface (more configuration options).
- Add ssreflect-like rewrite commands.
- Add record-type (as syntax sugar for Sigma-types).
- Implement inductive datatypes and recursive function package from first principles. The goal is to use the HOL/Isabelle approach.
- Generic Tableaux prover. - Generic Tableaux prover.
- [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework. - [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework.
- 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.