From ec7add0b48dee49255a9ac6ec3324ee81aaaebdd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 20 Sep 2025 01:06:05 -0700
Subject: [PATCH] doc: `!` modifier in `grind` parameters (#10474)

This PR adds a doc string for the `!` parameter modifier in `grind`.
---
 src/Init/Grind/Tactics.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 58487b172c..ce1afe2437 100644
--- 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