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: BitVec.toInt_srem #7699

Merged
merged 3 commits into from
Mar 29, 2025
Merged

feat: BitVec.toInt_srem #7699

merged 3 commits into from
Mar 29, 2025

Conversation

Rob23oba
Copy link
Contributor

This PR adds the BitVec.toInt_srem lemma, relating BitVec.srem with Int.tmod.

@Rob23oba Rob23oba requested a review from kim-em as a code owner March 27, 2025 16:30
@github-actions github-actions bot added changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Mar 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 27, 2025 •
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 7bd937580494311ecdb9502a7b5ab0ccf473bd44 --onto 1465c23e12f6f8b608ef944be4559b1b5e38f40a. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-27 16:54:08)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7bd937580494311ecdb9502a7b5ab0ccf473bd44 --onto 060b2fe46fe728934744ee52271b92ab74cbd5b4. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-28 15:23:10)

TwoFX
TwoFX reviewed Mar 28, 2025
View reviewed changes
@tobiasgrosser
Copy link
Contributor

Nice. Thank you, @Rob23oba. These are elegant proofs. As @TwoFX said, please move the theorems into the relevant files. I am happy to help.

@Rob23oba
Copy link
Contributor Author

I moved most of the theorems to Lemmas.lean now and added some related lemmas.

tobiasgrosser
tobiasgrosser approved these changes Mar 28, 2025
View reviewed changes
Copy link
Contributor

@tobiasgrosser tobiasgrosser left a comment

Choose a reason for hiding this comment

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

LGTM. Thank you!

TwoFX
TwoFX approved these changes Mar 29, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

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

Thanks!

@TwoFX TwoFX added this pull request to the merge queue Mar 29, 2025
Merged via the queue into leanprover:master with commit 5348ce9 Mar 29, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

@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.
4 participants
@Rob23oba @leanprover-community-bot @tobiasgrosser @TwoFX