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

feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
Conversation 0 Commits 22 Files Changed 9 -3
1 changed files with 0 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit f3a3ca31a0 - Show all commits

3
Pantograph/Goal.lean
View File

@ -263,11 +263,8 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
state.restoreTacticM goal state.restoreTacticM goal
-- TODO: Fail if this is already in conv
-- See Lean.Elab.Tactic.Conv.convTarget -- See Lean.Elab.Tactic.Conv.convTarget
let convMVar ← Elab.Tactic.withMainContext do let convMVar ← Elab.Tactic.withMainContext do
-- TODO: Memorize this `rhs` as a conv resultant goal
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget) let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
Elab.Tactic.setGoals [newGoal.mvarId!] Elab.Tactic.setGoals [newGoal.mvarId!]
pure rhs.mvarId! pure rhs.mvarId!