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