lean2/doc/todo.md
2013-10-02 09:56:45 -07:00

1.7 KiB

To Do List

  • Add cast : Pi (A B : Type) (H : A = B) (a : A) : B, and implement "casting propagation" in the type checker.
  • Modify the let construct to store the type of the value. The idea is to allow let name : type := value in expr. The type does not need to be provided by the user. However, the user may want to provide it as a hint for the Lean elaborator.
  • Refactor the elaborator code. The elaborator will be one of the main data-structures in Lean. The elaborator manager should be shared between different frontends.
  • Reconsider whether meta-variables should be in expr or not. Metavariables (aka holes) are fundamental in our design.
  • Improve Lean pretty printer for Pi's. For example, it produces Var a : Pi (A : Type) (_ : A), A instead of Var a : Pi (A : Type), A -> A.
  • Decide what will be the main technique for customizing Lean's behavior. The elaborator manager will have many building blocks that can be put together in many different ways. Possible solutions:
    • We design our own configuration language.
    • We use an off-the-shelf embedded language such as Lua.
    • We use Lean itself.
  • Module for reading OpenTheory proofs.
  • Higher-Order unification and matching.
  • Rewriter (and Rewriter Combinators).
  • MCSat framework.
  • Implement independent type checker using a different programming language (e.g., OCaml).
  • Add match construct in expr.
  • Add inductive datatype (families) in the environment. It will be a new kind of object.
  • Add recursive function definition objects (low priority). It is another new kind of object.