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

test: Non-matchers are not matchers

This commit is contained in:
Leni Aniva 2025-04-03 11:18:17 -07:00
parent 1402a69eea
commit cf4a5955e3
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Test/Environment.lean
View File

@ -114,12 +114,20 @@ def test_symbol_location : TestT IO Unit := do
checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"] checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
checkTrue "constNames" $ constNames.contains "Nat.succ_add" checkTrue "constNames" $ constNames.contains "Nat.succ_add"
def test_matcher : TestT IO Unit := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
checkTrue "not matcher" $ ¬ Meta.isMatcherCore env `Nat.strongRecOn
def suite: List (String × IO LSpec.TestSeq) := def suite: List (String × IO LSpec.TestSeq) :=
[ [
("Catalog", test_catalog), ("Catalog", test_catalog),
("Symbol Visibility", test_symbol_visibility), ("Symbol Visibility", test_symbol_visibility),
("Inspect", test_inspect), ("Inspect", test_inspect),
("Symbol Location", runTest test_symbol_location), ("Symbol Location", runTest test_symbol_location),
("Matcher", runTest test_matcher),
] ]
end Pantograph.Test.Environment end Pantograph.Test.Environment