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

fix: Remove `calcPrevRhs?` in non-calc tactics

This commit is contained in:
Leni Aniva 2024-04-11 15:03:14 -07:00
parent 535770bbd7
commit 6b44d9ef14
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Pantograph/Goal.lean
View File

@ -34,6 +34,7 @@ structure GoalState where
-- Existence of this field shows that we are currently in `conv` mode. -- Existence of this field shows that we are currently in `conv` mode.
convMVar?: Option (MVarId × MVarId) := .none convMVar?: Option (MVarId × MVarId) := .none
-- Previous RHS for calc, so we don't have to repeat it every time -- Previous RHS for calc, so we don't have to repeat it every time
-- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
calcPrevRhs?: Option Expr := .none calcPrevRhs?: Option Expr := .none
protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
@ -139,6 +140,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
savedState := nextSavedState savedState := nextSavedState
newMVars := newMVarSet prevMCtx nextMCtx, newMVars := newMVarSet prevMCtx nextMCtx,
parentMVar? := .some goal, parentMVar? := .some goal,
calcPrevRhs? := .none,
} }
/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/ /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
@ -404,6 +406,7 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
state.savedState with state.savedState with
tactic := { goals := [goal] }, tactic := { goals := [goal] },
}, },
calcPrevRhs? := .none,
} }
/-- /--
@ -423,6 +426,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
term := state.savedState.term, term := state.savedState.term,
tactic := { goals := unassigned }, tactic := { goals := unassigned },
}, },
calcPrevRhs? := .none,
} }
/-- /--
Brings into scope all goals from `branch` Brings into scope all goals from `branch`