From aac39ca60c8da8fc2d807f94b0c177eb1e051ad9 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 23 Feb 2025 14:13:44 -0800
Subject: [PATCH] fix: Some test errors
---
Test/Metavar.lean | 2 +-
Test/Tactic/MotivatedApply.lean | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 276004b..421ea01 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -192,7 +192,7 @@ def test_proposition_generation: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
- #[.some "?m.29 x"])
+ #[.some "?m.30 x"])
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
let assign := "Eq.refl x"
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 2da643e..fbb1d7c 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
addTest $ ← conduit.withContext do
let t := toString (← Meta.ppExpr $ ← conduit.getType)
- return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
+ return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.150 ?m.{majorId}) = (n + 0 = n)")
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[