feat: BitVec.getMsbD_[ofNatLt|allOnes|not]

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

feat: BitVec.getMsbD_[ofNatLt|allOnes|not] #6149

Closed tobiasgrosser closed 4 days ago

tobiasgrosser commented 4 days ago

This PR completes the elementwise accessors for ofNatLt, allOnes, and not by adding their implementations of getMsbD.

tobiasgrosser commented 4 days ago

changelog-library

tobiasgrosser commented 4 days ago

@kim-em, adding changelog-library via PR comment works, but the CI must be re-triggered via a git push -f or sth similar, but the relevant CI task does not re-check automatically as the comment is added.

leanprover-community-bot commented 4 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 7fbe8e3b36faabc9cfcc45e65a4b7ef042c0b068. (2024-11-21 10:10:53)

kim-em commented 4 days ago

@kim-em, adding changelog-library via PR comment works, but the CI must be re-triggered via a git push -f or sth similar, but the relevant CI task does not re-check automatically as the comment is added.

Thanks for the report, I'll check it out. Strangely, adding the label by hand does automatically trigger CI again.