2013-09-13 17:01:40 +00:00
|
|
|
To Do List
|
|
|
|
|
----------
|
|
|
|
|
|
2014-02-07 01:01:30 +00:00
|
|
|
- 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.
|
2014-02-03 03:19:49 +00:00
|
|
|
- Generic Tableaux prover.
|
2013-09-15 06:07:40 +00:00
|
|
|
- [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework.
|
2014-02-03 03:19:49 +00:00
|
|
|
- Independent type checker using a different programming language (e.g., F* or OCaml).
|
|
|
|
|
- Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.
|
2014-02-07 01:01:30 +00:00
|
|
|
- Re-implement apply-tactic.
|
2014-02-08 17:23:13 +00:00
|
|
|
- Improve performance of `is_convertible` and `is_definitionally_equal` predicates.
|
2014-02-08 17:23:56 +00:00
|
|
|
- Create notation sets. We are currently puting all notation decls in a "single bag".
|
2014-02-08 17:23:13 +00:00
|
|
|
- Improve macro support, and allow users to provide arbitrary parser extensions using Lua.
|
