chore: add assertion

A global theorem should not have free variables in `symbols`.
leanprover · Dec 30, 2024 · 1f3919f · 1f3919f
1 parent 24a8561
commit 1f3919f
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean
@@ -288,6 +288,7 @@ def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr)
   let us := info.levelParams.map mkLevelParam
   let proof := mkConst declName us
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
+  assert! symbols.all fun s => s matches .const _
   trace[grind.pattern] "{declName}: {patterns.map ppPattern}"
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"