Sort
0.2.4
100%
- Allow deletion of individual proof states
- Most robust bookkeeping for proof states
- Allow monitoring of current resource usage so the client can know when bookkeeping becomes necessary (rather than waiting for the thing to crash and having to rebuild all proof states)
- Add pre-commit hooks to run the tests and check for white space usage
0.2.6
100%
- Allow hole filing ("Agda style") proof and expression generation
- Add more serialization options
- Allow for more robust bookkeeping
0.2.7
100%
Simplify expression serialization
0.2.8
100%
- Selectively continue goals
0.2.9
100%
- Fix error formatting
- Output dependency
0.2.10
100%
Minor serialization update:
- Print
Expr.projas function applications w.r.t. the projector of a structure - Print "private" symbols, which proofs somehow depend on, in the catalog. However unsafe and symbols in the
Lean.namespace should not be printed.
0.2.12
100%
- Print information about inducts, recursors, and constructors in
env.inspect.