aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
Conversation 6 Commits 41 Files Changed 22 +4 -1
2 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 2937675044 - Show all commits

2
Pantograph/Goal.lean
View File

@ -521,7 +521,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
| .ok syn => pure syn
| .error error => return .parseError error
state.execute goalId (tacticM := Tactic.motivatedApply recursor)
protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: String):
protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with

3
Pantograph/Library.lean
View File

@ -208,5 +208,8 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
@[export pantograph_goal_motivated_apply_m]
def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
runTermElabM <| state.tryMotivatedApply goalId recursor
@[export pantograph_goal_no_confuse_m]
def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
runTermElabM <| state.tryNoConfuse goalId recursor
end Pantograph