fix: getTheoremKindFromOpt

leanprover · Jan 17, 2025 · be16ca1 · be16ca1
1 parent 9fe4400
commit be16ca1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -692,7 +692,7 @@ def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do
   if stx[1].isNone then
     return .default
   else
-    getTheoremKindCore stx[1]
+    getTheoremKindCore stx[1][0]
 
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do
   if (← getConstInfo declName).isTheorem then