0.3

  • feat(env): Allow adding definitions/theorems to the environment
  • chore: Stabilize Lean to at least version 4.8.0 4.12.0 4.14.0
  • feat(goal): Add support for the have, conv, calc tactics
  • feat(frontend): Add proof scraping support
  • feat(goal): Add synthetic tactics (motivated apply, no confuse, etc.)
  • feat: Add condensed delated interface
  • feat(goal): Add automatic mode
  • feat(serial): Add environment/state pickling
  • doc: Add design rational documentation
  • feat(goal): Articulation of finished proof term (could be very ugly)
2025-01-15
83% Completed