2024-07-04T21:54:48Z - 2024-10-04T21:54:48Z
Overview
1 Release published by 1 user
Published
v0.2.18
12 Pull requests merged by 1 user
Merged
#99 feat: Collect holes in Lean file and put them into a GoalState
Merged
#100 fix: Tactics should produce .syntheticOpaque goals
Merged
#101 feat: Set automaticMode to true by default
Merged
#92 feat: Automatic Mode
Merged
#94 feat: Expose GoalState functions
Merged
#96 doc: Add GPL License
Merged
#91 fix: Instantiate type when detecting eq
Merged
#90 fix: Bindings in prograde tactics
Merged
#83 feat: Prograde tactics
Merged
#87 test: Use lake test. Retired Makefile
Merged
#85 feat: Condensed interface
Merged
#86 chore: Update Lean to v4.10.0-rc1
1 Pull request proposed by 1 user
Proposed
#105 feat: Remove most filters on catalog
8 Issues closed from 1 user
Closed
#97 Parse and enter environment at arbitrary points of the input
Closed
#103 Metavariable not found bug with sorry collection
Closed
#93 Refactor out the Pantograph executable and lib into different targets
Closed
#88 Resumption not taking type unification into account
Closed
#74 Enable direct expression evaluation in context
Closed
#67 Extraction of atomization step
Closed
#80 Expose the String.toName interface
Closed
#84 Move towards Expr based interface
4 Issues created by 1 user
Opened
#95 Pickling
Opened
#98 Use MLList from Batteries
Opened
#102 Timeout for tactics
Opened
#104 goal.delete exceeds max recursion depth
2 Unresolved Conversations
Open
#78
Add option for Meta.ppGoal
Open
#23
Printing fine-grained delaboration structure