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

fix: Remove unused variable

This commit is contained in:
Leni Aniva 2025-01-24 19:06:07 -08:00
parent b67d3eccc4
commit 418d630255
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Test/Environment.lean
View File

@ -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"