From b45b90b810c845629788eca844a68873305bd1fd Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 12 Apr 2024 21:41:16 -0700
Subject: [PATCH] test: Metavariable name matches in let

---
 Test/Proofs.lean | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 4f81085..ad22e8d 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -564,20 +564,25 @@ def test_let (specialized: Bool): TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[interiorGoal [] "p ∨ ¬p"])
 
-  let expr := "let b: Nat := _; _"
+
+  let letType := "Nat"
+  let expr := s!"let b: {letType} := _; _"
   let result2 ← match specialized with
-    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := "Nat")
+    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
     | false => state1.tryAssign (goalId := 0) (expr := expr)
   let state2 ← match result2 with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check expr ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+  let serializedState2 ← state2.serializeGoals (options := ← read)
+  addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
     #[
-      interiorGoal [] "Nat",
+      interiorGoal [] letType,
       interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
     ])
+  -- Check that the goal mvar ids match up
+  addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
 
   let tactic := "exact a"
   let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with