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 +2 -2
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 679871cbc6 - Show all commits

4
Pantograph/Library.lean
View File

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