Skip to content

doc: fix typo in Format.bracketFill documentation#14018

Open
ia0 wants to merge 1 commit into
leanprover:masterfrom
ia0:typo2
Open

doc: fix typo in Format.bracketFill documentation#14018
ia0 wants to merge 1 commit into
leanprover:masterfrom
ia0:typo2

Conversation

@ia0

@ia0 ia0 commented Jun 11, 2026

Copy link
Copy Markdown

This PR fixes the documentation of Format.bracketFill to say that Format.bracket should be used for allOrNone. This was probably a copy/paste oversight from the documentation of Format.bracket.

This PR fixes the documentation of `Format.bracketFill` to say that `Format.bracket` should be used for `allOrNone`. This was probably a copy/paste oversight from the documentation of `Format.bracket`.
@ia0 ia0 requested a review from kim-em as a code owner June 11, 2026 19:09
@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 45c6939e5f66d98e27e72729edd8483d8e62a2c2 --onto d2f48db30713019241520218d0965227bbb64eed. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-11 19:49:01)

@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 45c6939e5f66d98e27e72729edd8483d8e62a2c2 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-11 19:49:03)

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.

2 participants