From 5e61282660c72397d478b66eddee60add989679f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 Jan 2025 10:30:26 -0800 Subject: [PATCH] test: Source location extraction --- Test/Environment.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Test/Environment.lean b/Test/Environment.lean index af98c10..b646279 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -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" checkEq "module" result.module? <| .some "Init.Data.Nat.Basic" - -- Doesn't work for symbols in `Init` for some reason - --checkEq "file" result.sourceUri? <| .some "??" + -- Extraction of source doesn't work for symbols in `Init` for some reason + checkTrue "file" result.sourceUri?.isNone checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0 checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88