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