Skip to content

fix: add missing pp-spaces in grind_pattern#11686

Merged
kim-em merged 3 commits intoleanprover:masterfrom
adomani:adomani/pp_in_grind_pattern
Mar 17, 2026
Merged

fix: add missing pp-spaces in grind_pattern#11686
kim-em merged 3 commits intoleanprover:masterfrom
adomani:adomani/pp_in_grind_pattern

Conversation

@adomani
Copy link
Contributor

@adomani adomani commented Dec 15, 2025

This PR adds a pretty-printed space in grind_pattern.

#lean4 > Some pretty printing quirks @ 💬

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 15, 2025
@ghost
Copy link

ghost commented Dec 15, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 949cf6924649a3ad3aa934ee4466438bd6994064 --onto 6a0b0c8273ab560d093494a2daa4dd3088437ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-15 18:19:44)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-23 11:26:59)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 15, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 949cf6924649a3ad3aa934ee4466438bd6994064 --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-15 18:19:45)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-23 11:27:01)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9e0aa14b6fe1420e0efaffce961c5b21b49c90dc --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-17 03:57:29)

@grunweg
Copy link
Contributor

grunweg commented Dec 15, 2025

Seems sensible to me, thanks!

@kim-em kim-em marked this pull request as ready for review January 8, 2026 01:44
@kim-em kim-em requested a review from leodemoura as a code owner January 8, 2026 01:44
@kim-em kim-em enabled auto-merge January 8, 2026 01:44
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9e0aa14b6fe1420e0efaffce961c5b21b49c90dc --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-17 03:57:27)

@kim-em kim-em added the changelog-language Language features and metaprograms label Mar 17, 2026
@kim-em kim-em added this pull request to the merge queue Mar 17, 2026
@kim-em kim-em added changelog-no Do not include this PR in the release changelog and removed changelog-language Language features and metaprograms labels Mar 17, 2026
Merged via the queue into leanprover:master with commit 6b60462 Mar 17, 2026
32 of 33 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants