Labels Milestones

2 Open 14 Closed

Sort

Earliest due date Latest due date Least complete Most complete Most issues Least issues

0.2.25

45%

6 Open

5 Closed

Updated 2025-01-17 23:11:39 -08:00

2025-01-30

• feat(goal): Draft tactic
• fix(goal): Prohibit coupling in draft tactics and drafting
• feat(serial): Pickle environment extensions in goal state
• feat(environment): Reading module and import data
• chore: Update Lean to v4.14.0 v4.15.0
• fix(delate): Panic of projection normalization function

0.3

92%

3 Open

37 Closed

Updated 2025-01-18 12:16:49 -08:00

2025-02-15

• 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)