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|toFin|getMsbD]_ofBool #6317

Merged
merged 5 commits into from
Dec 10, 2024
Merged

feat: BitVec.[toInt|toFin|getMsbD]_ofBool #6317

merged 5 commits into from
Dec 10, 2024

Conversation

tobiasgrosser
Copy link
Contributor

This PR completes the basic API for BitVec.ofBool.

@tobiasgrosser tobiasgrosser requested a review from kim-em as a code owner December 5, 2024 05:11
@tobiasgrosser
Copy link
Contributor Author

changelog-library

@github-actions github-actions bot added the changelog-library Library label Dec 5, 2024
@tobiasgrosser
feat: BitVec.[toInt|toFin|getMsbD]_ofBool
34ff1df 
This PR completes the basic API for the BitVec.ofBool function.
@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 Dec 5, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 5, 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 f6e88e5a0525b744c5df018dd96d2f0cbca29435 --onto c5181569f959e4a0d9586954212125adcb6e44d0. (2024-12-05 05:42:21)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c333ef9695c23f2ea02dae7a4b80fd9e567ea75 --onto 3f791933f16d74d74ab8116c96cadec6cdf7b70e. (2024-12-10 02:49:09)

@leanprover-bot leanprover-bot added the P-high We will work on this issue label Dec 6, 2024
@kim-em kim-em self-assigned this Dec 10, 2024
@kim-em
Copy link
Collaborator

kim-em commented Dec 10, 2024

Could you rearrange the theorems so that these are adjacent to the other ofBool accessors, e.g. getLsbD_ofBool?

@kim-em kim-em added the awaiting-author Waiting for PR author to address issues label Dec 10, 2024
@tobiasgrosser
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Dec 10, 2024
@kim-em kim-em removed the awaiting-review Waiting for someone to review the PR label Dec 10, 2024
@kim-em kim-em added this pull request to the merge queue Dec 10, 2024
Merged via the queue into leanprover:master with commit 1786539 Dec 10, 2024
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees

@kim-em kim-em

Labels
changelog-library Library P-high We will work on this issue 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
@tobiasgrosser @leanprover-community-bot @kim-em @leanprover-bot