8000 feat: bv_decide add rewrites around ite + operations by hargoniX · Pull Request #7298 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: bv_decide add rewrites around ite + operations #7298

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
Merged
merged 5 commits into from
Mar 3, 2025
Merged

feat: bv_decide add rewrites around ite + operations #7298

merged 5 commits into from
Mar 3, 2025

Conversation

hargoniX
Copy link
Contributor
@hargoniX hargoniX commented Mar 3, 2025

This PR adds rewrites to bv_decide's preprocessing that concern combinations of if-then-else and operation such as multiplication or negation.

@hargoniX hargoniX added the changelog-language Language features, tactics, and metaprograms label Mar 3, 2025
@hargoniX hargoniX requested a review from kim-em as a code owner March 3, 2025 10:23
@bollu
Copy link
Contributor
bollu commented Mar 3, 2025

LGTM :)

@hargoniX hargoniX enabled auto-merge March 3, 2025 10:28
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 3, 2025 10:36 Inactive
@hargoniX hargoniX added this pull request to the merge queue Mar 3, 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 Mar 3, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7298
a3a8e62
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7298
e575a24
Merged via the queue into master with commit 7836712 Mar 3, 2025
16 checks passed
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 3, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@hargoniX hargoniX deleted the hbv/bv_decide_more_if branch March 3, 2025 12:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

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.
3 participants
@hargoniX @bollu @leanprover-community-bot
0