test: Add test for module read
This commit is contained in:
parent
bc4bf47c8b
commit
be8dee6731
|
@ -110,6 +110,9 @@ 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"
|
||||
checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
|
||||
checkTrue "constNames" $ constNames.contains "Nat.succ_add"
|
||||
|
||||
def suite: List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
|
|
Loading…
Reference in New Issue