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

test(goal): Collision of aux lemma names

This commit is contained in:
Leni Aniva 2025-06-26 16:41:49 -07:00
parent f914e161e8
commit 349cff6f05
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
2 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Pantograph/Goal.lean
View File

@ -136,8 +136,9 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n]
Meta.mapMetaM <| state.withContext' state.root Meta.mapMetaM <| state.withContext' state.root
private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit := private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
let { nextMacroScope, ngen, .. } := state
modifyGetThe Core.State (fun st => ((), modifyGetThe Core.State (fun st => ((),
{ st with nextMacroScope := state.nextMacroScope, ngen := state.ngen })) { st with nextMacroScope, ngen }))
-- Restore the name generator and macro scopes of the core state -- Restore the name generator and macro scopes of the core state
protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
restoreCoreMExtra state.coreState restoreCoreMExtra state.coreState

1
Test/Metavar.lean
View File

@ -291,6 +291,7 @@ def test_replay_environment : TestM Unit := do
pure type pure type
let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "left" let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "left"
state.restoreMetaM
let goal := state.goals[1]! let goal := state.goals[1]!
let type ← goal.withContext do let type ← goal.withContext do
let .ok type ← elabTerm (← `(term|(3: Nat) ≤ 5)) (.some $ .sort 0) | unreachable! let .ok type ← elabTerm (← `(term|(3: Nat) ≤ 5)) (.some $ .sort 0) | unreachable!