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: UIntX.toBitVec lemmas #6625

Merged
merged 3 commits into from
Jan 13, 2025
Merged

feat: UIntX.toBitVec lemmas #6625

merged 3 commits into from
Jan 13, 2025

Conversation

hargoniX
Copy link
Contributor

This PR adds lemmas describing the behavior of UIntX.toBitVec on UIntX operations.

I did not define them for the IntX half yet as that lemma file is non existent so far and we can start working on UIntX in bv_decide with this, then add IntX when we grow the IntX API.

@hargoniX hargoniX added the changelog-library Library label Jan 13, 2025
@hargoniX hargoniX requested a review from TwoFX January 13, 2025 10:52
@hargoniX hargoniX requested a review from kim-em as a code owner January 13, 2025 10:52
TwoFX
TwoFX approved these changes Jan 13, 2025
View reviewed changes
src/Init/Data/UInt/Lemmas.lean Outdated Show resolved Hide resolved
@hargoniX hargoniX enabled auto-merge January 13, 2025 12:01
@hargoniX hargoniX disabled auto-merge January 13, 2025 12:21
@hargoniX hargoniX enabled auto-merge January 13, 2025 12:24
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 13, 2025 12:34 Inactive
@hargoniX hargoniX added this pull request to the merge queue Jan 13, 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 Jan 13, 2025
@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 2421f7f79941853da14346a234aec6df70cf36a1 --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-13 12:52:03)

@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jan 13, 2025
@hargoniX hargoniX added this pull request to the merge queue Jan 13, 2025
@hargoniX
Copy link
Contributor Author

(error was only some netlify flipper)

@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jan 13, 2025
@hargoniX hargoniX added this pull request to the merge queue Jan 13, 2025
Merged via the queue into master with commit 734fca7 Jan 13, 2025
15 checks passed
@hargoniX hargoniX deleted the hbv/uintx-to-bitvec branch January 13, 2025 15:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX approved these changes

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

Assignees
No one assigned
Labels
changelog-library Library 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 @TwoFX