From cf4a5955e3c971c99fe1e929f2507ee710c62a00 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 3 Apr 2025 11:18:17 -0700
Subject: [PATCH] test: Non-matchers are not matchers

---
 Test/Environment.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Test/Environment.lean b/Test/Environment.lean
index be4bd0a..a8f6cc5 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -114,12 +114,20 @@ def test_symbol_location : TestT IO Unit := do
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     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) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
     ("Symbol Location", runTest test_symbol_location),
+    ("Matcher", runTest test_matcher),
   ]
 
 end Pantograph.Test.Environment