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

fix(tactic): Erase finished calc goal #228

Open
aniva wants to merge 1 commits from fix/calc-erase-goal into dev
pull from: fix/calc-erase-goal
merge into: aniva:dev
Conversation 0 Commits 1 Files Changed 1 +2 -1
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Pantograph/Tactic/Fragment.lean
View File

@ -144,11 +144,12 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (
unless ← Meta.isDefEq proofType target do throwFailed unless ← Meta.isDefEq proofType target do throwFailed
remainder? := .some lastStepGoal.mvarId! remainder? := .some lastStepGoal.mvarId!
goal.assign proof goal.assign proof
let map := map.erase goal
let goals := [ mvarBranch ] ++ remainder?.toList let goals := [ mvarBranch ] ++ remainder?.toList
Elab.Tactic.setGoals goals Elab.Tactic.setGoals goals
match remainder? with match remainder? with
| .some goal => return map.erase goal |>.insert goal $ .calc (.some rhs) | .some goal => return map.insert goal $ .calc (.some rhs)
| .none => return map | .none => return map
| .conv .. => do | .conv .. => do
throwError "Direct operation on conversion tactic parent goal is not allowed" throwError "Direct operation on conversion tactic parent goal is not allowed"