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: add BitVec.toNat_[abs|sdiv|smod] #5491

Merged
merged 10 commits into from
Sep 27, 2024
Merged

feat: add BitVec.toNat_[abs|sdiv|smod] #5491

merged 10 commits into from
Sep 27, 2024

Conversation

tobiasgrosser
Copy link
Contributor

No description provided.

@tobiasgrosser tobiasgrosser marked this pull request as ready for review September 27, 2024 07:55
luisacicolini
luisacicolini approved these changes Sep 27, 2024
View reviewed changes
Copy link
Contributor

@luisacicolini luisacicolini left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

@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 Sep 27, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9eef72620448dc267188d954514b4548d909fc52 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 08:27:27)

hargoniX
hargoniX requested changes Sep 27, 2024
View reviewed changes
Copy link
Contributor

@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm assuming the reason that you didn't put these theorems in the bv_toNat simp set is that omega cannot handle match and if yes? Apart from that it looks fine to me.

@tobiasgrosser
Copy link
Contributor Author

I'm assuming the reason that you didn't put these theorems in the bv_toNat simp set is that omega cannot handle match and if yes? Apart from that it looks fine to me.

Right. However, on reflection it still makes sense. The pattern will then just be to call bv_toNat, then split on the cases, use omega after.

@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9eef72620448dc267188d954514b4548d909fc52 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 09:39:00)

@hargoniX hargoniX added this pull request to the merge queue Sep 27, 2024
Merged via the queue into leanprover:master with commit 0733273 Sep 27, 2024
13 checks passed
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Sep 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hargoniX hargoniX hargoniX approved these changes

@luisacicolini luisacicolini luisacicolini approved these changes

Assignees
No one assigned
Labels
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.
5 participants
@tobiasgrosser @leanprover-community-bot @hargoniX @luisacicolini @leanprover-bot