Skip to content

feat: enable disjunctive side-conditions of grind_pattern #11791

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
pirapira wants to merge 14 commits into from
Closed

feat: enable disjunctive side-conditions of grind_pattern #11791

pirapira wants to merge 14 commits into from
+204 −53

Conversation

@pirapira
Copy link

@pirapira pirapira commented Dec 24, 2025 •
edited
Loading

This PR enables use or <|> as disjunction in side-conditions of grind_pattern, where disjuncts cannot be guard or check.

Closes #11602.

@pirapira pirapira mentioned this pull request Dec 24, 2025
Open
@pirapira pirapira changed the title feat: Disjunctive side-conditions of grind_pattern feat: enable disjunctive side-conditions of grind_pattern Dec 24, 2025
@pirapira
fix: use <|> instead of or
3b92304 
Produced with Sonnet-4.5
@pirapira
fix: recover tests
ae53f5c 
Produced with Sonnet-4.5
@pirapira
Copy link
Author

pirapira commented Dec 24, 2025

changelog-feat

@github-actions github-actions bot added changelog-feat toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Dec 24, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 24, 2025

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-24 19:58:39)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 24, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-24 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-24 19:58:40)

@kim-em
Copy link
Collaborator

kim-em commented Jan 9, 2026

We are not intending to merge this.

@kim-em kim-em added the closing soon This issue will be closed soon (<1 month) as it is missing essential features. label Jan 9, 2026
@pirapira
Copy link
Author

pirapira commented Jan 9, 2026

Thank you for the organization.

@pirapira pirapira closed this Jan 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

No one assigned

Labels

changelog-feat closing soon This issue will be closed soon (<1 month) as it is missing essential features. 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.

RFC: disjunction of guard conditions for grind_pattern

4 participants

@pirapira @leanprover-community-bot @leanprover-bot @kim-em