Skip to content

Latest commit

 

History

History
19 lines (18 loc) · 1.03 KB

todo.md

File metadata and controls

19 lines (18 loc) · 1.03 KB
Raw

To Do List

  • 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.
  • Create notation sets. We are currently puting all notation decls in a "single bag".
  • Improve macro support, and allow users to provide arbitrary parser extensions using Lua.