Skip to content
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

feat: bv_decide support enum inductive matches with default branches #7417

Merged
merged 6 commits into from
Mar 10, 2025
Merged

feat: bv_decide support enum inductive matches with default branches #7417

merged 6 commits into from
Mar 10, 2025

Conversation

hargoniX
Copy link
Contributor

This PR adds support for enum inductive matches with default branches to bv_decide.

@hargoniX hargoniX added the changelog-language Language features, tactics, and metaprograms label Mar 10, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 10, 2025 12:55 Inactive
@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 Mar 10, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7417
2869419
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7417
9b5cf86
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 10, 2025 13:41 Inactive
@hargoniX hargoniX enabled auto-merge March 10, 2025 13:42
@hargoniX hargoniX added this pull request to the merge queue Mar 10, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 10, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7417
a6b0f79
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7417
1caeaba
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 10, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 10, 2025 •
edited
Loading

Mathlib CI status (docs):

Merged via the queue into master with commit e0fa6a1 Mar 10, 2025
20 checks passed
@hargoniX hargoniX deleted the hbv/enum_inductive_default_reorder branch March 10, 2025 17:30
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
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, 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
@hargoniX @leanprover-community-bot