Skip to content

feat: enable notationItem in "mixfix" notation commands#10378

Merged
kmill merged 1 commit intoleanprover:masterfrom
kmill:kmill_1056_2
Sep 14, 2025
Merged

feat: enable notationItem in "mixfix" notation commands#10378
kmill merged 1 commit intoleanprover:masterfrom
kmill:kmill_1056_2

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Sep 14, 2025 •
edited
Loading

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:

infixr:30 unicode(" ∨ ", " \\/ ") => Or

Continuation of #10373.

@kmill
feat: enable notationItem in mixfix notation commands
2268d8e 
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
@kmill kmill added the changelog-language Language features and metaprograms label Sep 14, 2025
@kmill kmill changed the title feat: enable notationItem in mixfix notation commands feat: enable notationItem in "mixfix" notation commands Sep 14, 2025
@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 Sep 14, 2025
@ghost
Copy link
Copy Markdown

ghost commented Sep 14, 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 3146f6c6517eded3f05b51c107a6f8d9efa20291 --onto b64111d5a837bb5273978cf9945bb137a31777b7. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-14 17:15:18)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 14, 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 3146f6c6517eded3f05b51c107a6f8d9efa20291 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-14 17:15:20)

@kmill kmill added this pull request to the merge queue Sep 14, 2025
Merged via the queue into leanprover:master with commit 02a4713 Sep 14, 2025
25 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kmill @leanprover-bot