doc: ! modifier in grind parameters

This PR adds a doc string for the `!` parameter modifier in `grind`.
2026-04-13 23:54:10 +00:00 · 2025-09-20 00:58:46 -07:00
1 changed files with 4 additions and 1 deletions
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -182,7 +182,10 @@ namespace Lean.Parser.Tactic

 syntax grindErase    := "-" ident
 syntax grindLemma    := ppGroup((Attr.grindMod ppSpace)? ident)
-- `!` for enabling minimal indexable subexpression restriction
+/--
+The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
+when selecting patterns.
+-/
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
 syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin