From 6323c02f47872194efd8a8c0c2f9c8aa4ecdc7a6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 20 Jun 2025 12:25:40 -0700 Subject: [PATCH] test: Fix pickle state name --- Test/Serial.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/Serial.lean b/Test/Serial.lean index 55170dc..64717b9 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -89,7 +89,7 @@ def test_pickling_env_extensions : TestM Unit := do let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable! let parentExpr := state1.parentExpr?.get! checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma - goalStatePickle state statePath + goalStatePickle state1 statePath let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do let (state1, _) ← goalStateUnpickle statePath (← getEnv) let parentExpr := state1.parentExpr?.get!