feat: add unicode(...) parser syntax and pp.unicode option#10373
Merged
kmill merged 2 commits intoleanprover:masterfrom Sep 14, 2025
Merged
feat: add unicode(...) parser syntax and pp.unicode option#10373kmill merged 2 commits intoleanprover:masterfrom
unicode(...) parser syntax and pp.unicode option#10373kmill merged 2 commits intoleanprover:masterfrom
Conversation
This PR adds a `pp.unicode` option and a `unicode("→", "->")` syntax for syntax descriptions, for the lower-level `unicodeSymbol "→" "->"` parser. The syntax is added to the `notation` command as well. When `pp.unicode` is true (the default) then the first form is used when pretty printing, and otherwise the second ASCII form is used. A variant, `unicode("→", "->", preserveForPP)` causes the `->` form to be preferred; delaborators can insert `→` directly into the syntax, which will be pretty printed; this allows notations like `fun` to use custom options such as `pp.unicode.fun` to opt in to the unicode form when pretty printing.
- Adds more documentation for the `symbol` and `nonReservedSymbol` parser descriptions.
- Adds documentation for the `infix`/`infixr`/`infixl`/`prefix`/`postfix` commands.
- The parenthesizers for symbols are improved to backtrack if the atom doesn't match.
- Fixes a bug where `&"..."` symbols aren't validated.
This is partial progress for issue leanprover#1056. What remains is enabling `unicode(...)` for mixfix commands and then making use of it for core notation.
Collaborator
|
Reference manual CI status:
|
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 14, 2025
ghost
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 14, 2025
|
Mathlib CI status (docs):
|
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Sep 14, 2025
This PR enables using `notation` items in `infix`/`infixl`/`infixr`/`prefix`/`postfix`. The motivation for this is to enable being able to use `pp.unicode`-aware parsers. A followup PR can combine core parsers as such:
```lean
infixr:35 unicode(" ∨ ", " \\/ ") => Or
```
Continuation of leanprover#10373
github-merge-queue bot
pushed a commit
that referenced
this pull request
Sep 14, 2025
This PR enables using `notation` items in
`infix`/`infixl`/`infixr`/`prefix`/`postfix`. The motivation for this is
to enable being able to use `pp.unicode`-aware parsers. A followup PR
can combine core parsers as such:
```lean
infixr:30 unicode(" ∨ ", " \\/ ") => Or
```
Continuation of #10373.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Sep 14, 2025
This PR sets the `syntax` naming heuristic for `unicode(" → ", " -> ")` to use `→` rather than `→->`.
Continuation of leanprover#10373.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Sep 14, 2025
This PR sets the `syntax` naming heuristic for `unicode(" → ", " -> ")`
to use `→` rather than `→->`.
Continuation of #10373.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Sep 15, 2025
This PR makes notations such as `∨`, `∧`, `≤`, and `≥` pretty print using ASCII versions when `pp.unicode` is false. Continuation of leanprover#10373. Closes leanprover#1056.
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 15, 2025
* fix deprecations * remove upstreamed defs * two fixes * fix merge * fix merge * revert sqrt changes * ugh * fix from nightly-testing * fix merge * remove test deleted on master * fix test * note about test * . * Update lean-toolchain for leanprover/lean4#10194 * chore: bump to nightly-2025-09-02 * adjust to upstream changes * fix * fix * long line * Use Mathlib's nightly toolchain to run docgen in the nightly test * simpNF linter * whitespace * Update lean-toolchain for testing leanprover/lean4#10217 * Correct the working directory: should be 'docbuild' * Rework the grind regression report as a nightly-testing regression report It should still report the same things, but now as one message for all regression kinds * feat(Cache): download speeds & more info on errors * fix(Cache): add base download failure message * fixes * turn off linter * adaptation note * turn off linter.nightlyRegressionSet * chore: adaptations for nightly-2025-09-02 * Update lean-toolchain for testing leanprover/lean4#10059 * Update lean-toolchain for leanprover/lean4#10217 * chore: bump to nightly-2025-09-03 * Remove the erroring nightly regression report, we'll develop this on another branch. * fixes * update LibraryRewrite test * Update lean-toolchain for leanprover/lean4#10059 * chore: bump to nightly-2025-09-04 * fix * chore: bump to nightly-2025-09-05 * chore: adaptations for nightly-2025-09-05 * chore: bump to nightly-2025-09-06 * Update lean-toolchain for testing leanprover/lean4#10271 * Adapt to leanprover/lean4#10271 * Bump batteries * Update lean-toolchain for leanprover/lean4#10271 * chore: bump to nightly-2025-09-07 * nolint unusedArguments * Merge master into nightly-testing * chore: bump to nightly-2025-09-08 * fixes * chore: bump to nightly-2025-09-09 * fix thing * Update lean-toolchain for testing leanprover/lean4#10306 * temporarily remove test * adaptation note * master version of Cache/Requests.lean * chore: bump to nightly-2025-09-10 * adaptation note * chore: adaptations for nightly-2025-09-10 * merge lean-pr-testing-10059 * bump toolchain manually?? * restore test * chore: bump to nightly-2025-09-11 * lake update * fix * adaptations for leanprover/lean4#10307 * remove validateDocComment in ToAdditive * remove upstreamed Function.Injective * update assert_not_exists * oops * comment out DeriveTraversable * chore: replace some grind attibutes with grind_pattern, to be robust for future heuristic changes * suggestions from Rob23oba * lshake --fix * fix bad shake * shake --update * . * chore: adaptations for nightly-2025-09-11 * chore: bump to nightly-2025-09-12 * Revert "oops" This reverts commit 517b832. * Revert "comment out DeriveTraversable" This reverts commit 0460eb8. * fix DeriveTraversable * add `binders` fields * fix * fixes * update manifest * fixes * fixes * fixes * chore: bump to nightly-2025-09-13 * fixes * fixes * fixes * fixes * fixes * fixes * fixes * remove adaptation note * Update lean-toolchain for testing leanprover/lean4#10373 * fixes * chore: bump to nightly-2025-09-14 * Update lean-toolchain for testing leanprover/lean4#10377 * fix * fix * fix * fix emrge * update batteries * chore: adaptations for nightly-2025-09-14 * Merge master into nightly-testing * Update Mathlib/Data/List/Basic.lean * Merge master into nightly-testing * chore: adaptations for nightly-2025-09-14 * chore: bump to nightly-2025-09-15 --------- Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Mar 9, 2026
This PR makes notations such as `∨`, `∧`, `≤`, and `≥` pretty print using ASCII versions when `pp.unicode` is false. Continuation of leanprover#10373. Closes leanprover#1056.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a
pp.unicodeoption and aunicode("→", "->")syntax description alias for the lower-levelunicodeSymbol "→" "->"parser. The syntax is added to thenotationcommand as well. Whenpp.unicodeis true (the default) then the first form is used when pretty printing, and otherwise the second ASCII form is used. A variant,unicode("→", "->", preserveForPP)causes the->form to be preferred; delaborators can insert→directly into the syntax, which will be pretty printed as-is; this allows notations likefunto use custom options such aspp.unicode.funto opt into the unicode form when pretty printing.Additionally:
symbolandnonReservedSymbolparser descriptions.infix/infixr/infixl/prefix/postfixcommands.&"..."symbols aren't validated.This is partial progress for issue #1056. What remains is enabling
unicode(...)for mixfix commands and then making use of it for core notation.