Labels Milestones

2 Open 13 Closed

Sort

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

0.2.24

0%

1 Open

0 Closed

Updated 2024-12-20 00:56:41 -08:00

2024-12-31

• feat(frontend): Extraction of symbol in source code position
• chore: Update Lean to v4.14.0
• fix(frontend): Divergence of behaviours between by sorry and sorry

0.3

83%

7 Open

35 Closed

Updated 2024-12-16 15:21:36 -08:00

2025-01-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)