lean2/doc/todo.md

To Do List

• Add heterogeneous equality back into the kernel.
• 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.
• MCSat framework.
• Independent type checker using a different programming language (e.g., F* or OCaml).
• Module for reading OpenTheory proofs.
• Re-implement apply-tactic.
• Improve performance of is_convertible and is_definitionally_equal predicates