chore: check whether declaration is a theorem or not

leanprover · Dec 29, 2024 · 83bb6be · 83bb6be
1 parent a0f73c3
commit 83bb6be
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean
@@ -160,8 +160,9 @@ def main (patterns : List Expr) : MetaM (List Expr × List HeadIndex) := do
 end NormalizePattern
 
 def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
-  let cinfo ← getConstInfo declName
-  let us := cinfo.levelParams.map mkLevelParam
+  let .thmInfo info ← getConstInfo declName
+    | throwError "`{declName}` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic"
+  let us := info.levelParams.map mkLevelParam
   let proof := mkConst declName us
   let (patterns, symbols) ← NormalizePattern.main patterns
   trace[grind.pattern] "{declName}: {patterns.map ppPattern}"

diff --git a/tests/lean/run/grind_pattern1.lean b/tests/lean/run/grind_pattern1.lean
@@ -18,3 +18,11 @@ info: [grind.pattern] List.mem_concat_self: [@Membership.mem #2 ? ? (@HAppend.hA
 -/
 #guard_msgs in
 grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
+
+def foo (x : Nat) := x + x
+
+/--
+error: `foo` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic
+-/
+#guard_msgs in
+grind_pattern foo => x + x