Skip to content

fix: format antiquotations on the left of trailing syntax - #15811

Merged
TwoFX merged 1 commit into
leanprover:masterfrom
TwoFX:antiquot-left
Oct 20, 2026
Merged

TwoFX merged 1 commit into
leanprover:masterfrom
TwoFX:antiquot-left

Conversation

@TwoFX

@TwoFX TwoFX commented Oct 20, 2026 •

Copy link
Copy Markdown
Member

This PR fixes the pretty-printer to be able to format antiquotations on the left of trailing syntax.

This requires tracking the relevant category. The way we do this is entirely analogous to the parenthesizer.

@TwoFX
TwoFX requested a review from kmill as a code owner October 20, 2026 12:20
@TwoFX TwoFX added the changelog-no Do not include this PR in the release changelog label Oct 20, 2026
@TwoFX
TwoFX enabled auto-merge October 20, 2026 12:20
@TwoFX
TwoFX added this pull request to the merge queue Oct 20, 2026
@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 Oct 20, 2026
Merged via the queue into leanprover:master with commit c5439dd Oct 20, 2026
25 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.

1 participant