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

test: Source location extraction

This commit is contained in:
Leni Aniva 2025-01-13 10:30:26 -08:00
parent 9d2a999a4f
commit 5e61282660
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Test/Environment.lean
View File

@ -106,8 +106,8 @@ def test_symbol_location : TestT IO Unit := do
let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed" let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
checkEq "module" result.module? <| .some "Init.Data.Nat.Basic" checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
-- Doesn't work for symbols in `Init` for some reason -- Extraction of source doesn't work for symbols in `Init` for some reason
--checkEq "file" result.sourceUri? <| .some "??" checkTrue "file" result.sourceUri?.isNone
checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0 checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88 checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88