Skip to content

fix: incorrect arrow orientations in grind syntax #8517

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
Closed
eric-wieser wants to merge 1 commit into from
Closed

fix: incorrect arrow orientations in grind syntax #8517

eric-wieser wants to merge 1 commit into from

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented May 28, 2025

This PR makes the ascii version of ← in the grind attribute be <- not -> (and vice versa for →)

@eric-wieser eric-wieser mentioned this pull request May 28, 2025
Closed
@eric-wieser
Copy link
Contributor Author

eric-wieser commented May 28, 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 May 28, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 28, 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 bd14e7079bfb39a87ecde0127974220d724e97c5 --onto 3af9ab64ed79a667fb8989f7a0c258b018aba371. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-28 16:18:00)

@eric-wieser eric-wieser reopened this May 28, 2025
@eric-wieser
Copy link
Contributor Author

eric-wieser commented May 28, 2025

(close/reopen to make CI notice the label)

@eric-wieser eric-wieser reopened this May 29, 2025
@Rob23oba
Copy link
Contributor

Rob23oba commented May 30, 2025 •
edited
Loading

(close/reopen to make CI notice the label)

An easier way is to push an empty commit (git commit --allow-empty) or (even easier) edit the description back and forth.
Edit: you can also remove delete label comments immediately after posting them.

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Jun 14, 2025
@eric-wieser eric-wieser closed this Jul 1, 2025
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 P-medium We may work on this issue if we find the time 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

@eric-wieser @leanprover-community-bot @Rob23oba @leanprover-bot