From 6b604625f24767720000546532477d343dd23755 Mon Sep 17 00:00:00 2001 From: damiano Date: Tue, 17 Mar 2026 04:15:02 +0000 Subject: [PATCH] fix: add missing pp-spaces in `grind_pattern` (#11686) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a pretty-printed space in `grind_pattern`. [#lean4 > Some pretty printing quirks @ 💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Some.20pretty.20printing.20quirks/near/563848793) Co-authored-by: Kim Morrison --- src/Lean/Meta/Tactic/Grind/Parser.lean | 2 +- tests/elab/ppSpaces.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Grind/Parser.lean b/src/Lean/Meta/Tactic/Grind/Parser.lean index 3cfe19c4e6..a3657438ed 100644 --- a/src/Lean/Meta/Tactic/Grind/Parser.lean +++ b/src/Lean/Meta/Tactic/Grind/Parser.lean @@ -138,7 +138,7 @@ example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by ``` -/ @[builtin_command_parser] def grindPattern := leading_parser - Term.attrKind >> "grind_pattern " >> optional ("[" >> ident >> "]") >> ident >> darrow >> sepBy1 termParser "," >> optional grindPatternCnstrs + Term.attrKind >> "grind_pattern " >> optional ("[" >> ident >> "]") >> ident >> darrow >> sepBy1 termParser ", " >> optional grindPatternCnstrs @[builtin_command_parser] def initGrindNorm := leading_parser "init_grind_norm " >> many ident >> "| " >> many ident diff --git a/tests/elab/ppSpaces.lean b/tests/elab/ppSpaces.lean index e9da141827..ec4d4e3c35 100644 --- a/tests/elab/ppSpaces.lean +++ b/tests/elab/ppSpaces.lean @@ -87,4 +87,9 @@ example : True := by { trivial } +/-- info: grind_pattern A => B, C -/ +#guard_msgs in +#pp +grind_pattern A => B, C + end Damiano1