fix: ground theorems as grind parameters

[leodemoura]

This PR ensures that ground theorems are properly handled as grind parameters. Additionally, grind [(thm)] and grind [thm] should be handled the same way.

[cursor]

This PR is being reviewed by Cursor Bugbot

Details

You are on the Bugbot Free tier. On this plan, Bugbot will review limited PRs each billing cycle.

To receive Bugbot reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

---

Bug: Missing syntax tracking for ground constructors in grind

When processing constructors via the .intro modifier (lines 140-141) or the inductive predicate loop in .infer (lines 155-157), if a constructor has zero parameters (like True.intro), it now goes to extraFacts due to the new ground theorem handling at lines 70-82. However, unlike other call sites (.ematch kind at 128-131, .infer else branch at 159-162), these loops don't track syntax in extraFactsSyntax. This means grind? suggestions would be incomplete when ground constructors are involved. The other call sites correctly check if extraFacts.size grew and push to extraFactsSyntax, but these two loops do not.

src/Lean/Elab/Tactic/Grind/Param.lean#L139-L141

lean4/src/Lean/Elab/Tactic/Grind/Param.lean

Lines 139 to 141 in d762aa1

	if incremental then throwError "`cases` parameter are not supported here"
	for ctor in info.ctors do
	params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable

src/Lean/Elab/Tactic/Grind/Param.lean#L154-L157

lean4/src/Lean/Elab/Tactic/Grind/Param.lean

Lines 154 to 157 in d762aa1

	-- we also add the constructors (intro rules) as E-matching rules
	for ctor in info.ctors do
	-- **Note**: We should not warn if `declName` is an inductive
	params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)

 

---