feat: add BitVec.[toNat|toInt|toFin|getLsbD|getMsbD|getElem|msb]_fill

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

Open tobiasgrosser opened 6 days ago

tobiasgrosser commented 6 days ago

This PR implements BitVec.*_fill.

tobiasgrosser commented 6 days ago

changelog-library

leanprover-community-bot commented 6 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 5145030ff4bed884213f584f8b2402be82e96d45 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-22 22:09:01)

kim-em commented 6 days ago

An alternative approch here might be to deprecate/delete fill. Do you know why we have it in the first place?