TODO.md

TODO's

LaTTe 0.x

• a usable proof assistant based on type theory [Done v.0.6.1-SNAPSHOT 10/2016]

LaTTe 1.x

• defimplicit for programmatic calculations on terms (replaces specials) [Done v0.99 - 10/2017]

• Opacity flag for definitions [Done v0.100.0 11/2017]

• explicit substitutions [Canceled (branch letstx) 11/2017]

• implicit goal hypotheses using _ [Done v0.101.0 11/2018]

• certificate generation and certified uberjars deployment [Done v0.102.0 11/2018]

• externalize and port library prelude [Done v0.103.0 11/2018]

• cleanup library prelude

• port library sets [Done v0.103.0 11/2018]

• cleanup library sets

• port library integers [Done v0.103.0 11/2018]

• cleanup library integers

• beta release(s)

• LaTTe tutorial

• finalize 1.0 documentation

• final release v1.0

LaTTe 2.x

... (incomplete, unordered, undecided) ...

• rewriting framework

• proof search and query

• proof refinement with holes

• library finite sets

• library finite sequences

• generic package for (co-)inductive definitions

LaTTe 3.X

... TBA ...