From 83bb6be1a1c90121388192c1d74cbe3a60c94a7a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 29 Dec 2024 12:11:24 -0800
Subject: [PATCH] chore: check whether declaration is a theorem or not

---
 src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean | 5 +++--
 tests/lean/run/grind_pattern1.lean              | 8 ++++++++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean
index 9e54c05a16db..4a9d2c9a20e5 100644
--- 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
index 1d3e93b8fd4b..79c3a564eb58 100644
--- 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