From 418d630255b2f78b0fcdf5257c244279d478f809 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 24 Jan 2025 19:06:07 -0800
Subject: [PATCH] fix: Remove unused variable

---
 Test/Environment.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Test/Environment.lean b/Test/Environment.lean
index c49cbae..e954bc3 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -110,7 +110,7 @@ def test_symbol_location : TestT IO Unit := do
     checkTrue "file" result.sourceUri?.isNone
     checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
     checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-    let .ok { imports, constNames, extraConstNames } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
+    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"