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: support udiv in bv_decide #5628

Merged
merged 6 commits into from
Oct 8, 2024
Merged

feat: support udiv in bv_decide #5628

merged 6 commits into from
Oct 8, 2024

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Oct 7, 2024

No description provided.

@hargoniX hargoniX force-pushed the hbv/bv_decide_udiv branch 3 times, most recently from 8d9cf50 to f2934aa Compare October 7, 2024 16:44
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 7, 2024 16:51 Inactive
@hargoniX hargoniX force-pushed the hbv/bv_decide_udiv branch from f2934aa to 64fdac3 Compare October 7, 2024 17:00
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 7, 2024 17:04 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 Oct 7, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 7, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1914a2b3f255107334f1fe9f0522cb089b45c39e --onto 9dac514c2fc80d3f60076314ad30a993a7b2c22f. (2024-10-07 17:23:11)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f1ff9cebf29edfc40fab70967274d3fb9b3cda1b --onto 9dac514c2fc80d3f60076314ad30a993a7b2c22f. (2024-10-07 18:31:06)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2ed7924baedeb3d262be786213a29ae51449db5d --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-08 10:08:01)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 7, 2024 17:32 Inactive
@hargoniX hargoniX force-pushed the hbv/bv_decide_udiv branch from 77bd117 to 4ddc3f8 Compare October 7, 2024 17:55
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 7, 2024 17:59 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 7, 2024 18:17 Inactive
bollu added a commit to opencompl/lean4 that referenced this pull request Oct 8, 2024
@bollu
chore: define udiv normal form to be %, resp. umod and %.
80fdd06 
This follows the norm for all other Bitvector operations,
and makes the symbolic version the simp normal form.

I would imagine that @hargoniX would prefer that this be merged
after leanprover#5628,
so as to prevent churn for his PR.
I'm happy to rebase the PR.
@bollu bollu mentioned this pull request Oct 8, 2024
Merged
hargoniX pushed a commit to opencompl/lean4 that referenced this pull request Oct 8, 2024
@bollu @hargoniX
chore: define udiv normal form to be %, resp. umod and %.
f1b996e 
This follows the norm for all other Bitvector operations,
and makes the symbolic version the simp normal form.

I would imagine that @hargoniX would prefer that this be merged
after leanprover#5628,
so as to prevent churn for his PR.
I'm happy to rebase the PR.
github-merge-queue bot pushed a commit that referenced this pull request Oct 8, 2024
@bollu @hargoniX
chore: define udiv normal form to be /, resp. umod and % (#5645)
2ed7924 
This follows the norm for all other Bitvector operations, and makes the
symbols `/` and `%` the simp normal form.

I'd imagine that @hargoniX would prefer that this be merged after
#5628, so as to prevent churn
for his PR. I'm happy to rebase the PR once the other PR lands.

---------

Co-authored-by: Henrik Böving <hargonix@gmail.com>
@hargoniX hargoniX force-pushed the hbv/bv_decide_udiv branch from d6e359c to 7bfd7c1 Compare October 8, 2024 09:45
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 8, 2024 09:52 Inactive
@hargoniX hargoniX marked this pull request as ready for review October 8, 2024 10:10
@hargoniX hargoniX enabled auto-merge October 8, 2024 10:26
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 8, 2024 10:34 Inactive
@hargoniX hargoniX added this pull request to the merge queue Oct 8, 2024
Merged via the queue into master with commit e9ea99f Oct 8, 2024
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bollu bollu bollu left review comments

Assignees
No one assigned
Labels
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 @leanprover-community-bot @bollu