Files
damiano 6b604625f2 fix: add missing pp-spaces in grind_pattern (#11686)
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 <kim@tqft.net>
2026-03-17 04:15:02 +00:00
..