feat: BitVec.[toInt|toFin]_concat and Bool.toInt

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

feat: BitVec.[toInt|toFin]_concat and Bool.toInt #6182

Open tobiasgrosser opened 6 days ago

tobiasgrosser commented 6 days ago

This PR adds BitVec.[toInt|toFin]_concat and moves a couple of theorems into the concat section, as BitVec.msb_concat is needed for the toInt_concat proof.

We also add Bool.toInt.

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 ba3f2b3ecf8967410f3498e2835b883601f03967 --onto 6202461a21d2636129cb8950cd9b6549ccf4b185. (2024-11-23 04:16:51)
🟡 Mathlib branch lean-pr-testing-6182 build against this PR was cancelled. (2024-11-29 05:33:41) View Log
✅ Mathlib branch lean-pr-testing-6182 has successfully built against this PR. (2024-11-29 06:27:43) View Log

tobiasgrosser commented 6 hours ago

awaiting-review