Skip to content

doc: fix typo in Format.nest example#14013

Merged
Kha merged 1 commit into
leanprover:masterfrom
ia0:typo
Jun 25, 2026
Merged

doc: fix typo in Format.nest example#14013
Kha merged 1 commit into
leanprover:masterfrom
ia0:typo

Conversation

@ia0

@ia0 ia0 commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

This PR fixes the example in the documentation of Format.nest. The documentation says that "the formatter will put in linebreaks after the commas", but before this PR it will put line breaks after the space following the commas. This seems like a typo in the example.

This PR fixes the example in the documentation of `Format.nest`. The documentation says that "the formatter will put in linebreaks after the commas", but before this PR it will put line breaks after the space following the commas. This seems like a typo in the example.
@ia0 ia0 requested a review from kim-em as a code owner June 11, 2026 15:24
@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 Jun 11, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d6ecb8918b0f249a37d717d0bafa0568ef93843a --onto d2f48db30713019241520218d0965227bbb64eed. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-11 16:11:48)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d6ecb8918b0f249a37d717d0bafa0568ef93843a --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-11 16:11:49)

@ia0

ia0 commented Jun 11, 2026

Copy link
Copy Markdown
Contributor Author

This PR indirectly impacts the manual, should I rebase it on nightly-with-manual?

@Kha Kha added this pull request to the merge queue Jun 25, 2026
Merged via the queue into leanprover:master with commit 5a9514e Jun 25, 2026
17 checks passed
@ia0 ia0 deleted the typo branch June 25, 2026 10:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

3 participants