Skip to content

feat: let by have the arg precedence #11455

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
JovanGerb wants to merge 8 commits into
base: master
Choose a base branch
from
Open

feat: let by have the arg precedence #11455

JovanGerb wants to merge 8 commits into from

Conversation

@JovanGerb
Copy link
Contributor

@JovanGerb JovanGerb commented Dec 1, 2025

This PR changes the precedence of by to the arg precedence. This means that it can be used as an argument directly, e.g h.trans by simp instead of h.trans <| by simp.

The source code claims that by already has the arg precedence:

/-- Precedence used for application arguments (`do`, `by`, ...). -/
macro "arg"  : prec => `(prec| 1023)

@JovanGerb
Copy link
Contributor Author

JovanGerb commented Dec 2, 2025

changelog-language

@github-actions github-actions bot added changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Dec 2, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 2, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-02 02:02:31)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11455
29f31a0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11455
e9034f9
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 2, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 2, 2025 •
edited
Loading

Mathlib CI status (docs):

@JovanGerb JovanGerb marked this pull request as draft December 2, 2025 04:32
Rob23oba
Rob23oba suggested changes Dec 2, 2025
View reviewed changes
src/Lean/Parser/Term.lean
register_parser_alias attrKind
register_parser_alias optSemicolon
register_parser_alias structInstFields

Copy link
Contributor

@Rob23oba Rob23oba Dec 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just add an alias here for termBeforeBy

Copy link
Contributor Author

@JovanGerb JovanGerb Dec 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does that require some kind of stage0 update? I.e. would it be easier to split that change out to a separate PR?

Copy link
Contributor

@Rob23oba Rob23oba Dec 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh right, I forgot. In that case, you can add the alias but keep the #check_tactic parser as you have now, and then we can clean it up after a stage0 update (but also edit stage0/src/stdlib_flags.h to trigger a stage0 update)

@JovanGerb JovanGerb marked this pull request as ready for review December 3, 2025 02:23
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11455
af6515c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11455
46d018a
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 3, 2025
@JovanGerb
Copy link
Contributor Author

JovanGerb commented Dec 3, 2025

It seems that a test in mathlib is breaking for the same reason as some tests over here. To avoid having to change the imports in the test file, should this PR be split up with a stage0 in between? The first part would be just initializing the termBeforeBy parser.

@Rob23oba
Copy link
Contributor

Rob23oba commented Dec 3, 2025

Hmm right, that might be simpler than doing all of the changes with #check_tactic and undoing them later

@JovanGerb
Copy link
Contributor Author

JovanGerb commented Dec 3, 2025

All right, I have made #11495

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@Rob23oba Rob23oba Rob23oba requested changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR 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.

4 participants

@JovanGerb @leanprover-bot @leanprover-community-bot @Rob23oba