chore: delete double namespace BitVec.BitVec

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.88k stars 329 forks source link

Closed bollu closed 2 weeks ago

bollu commented 2 weeks ago

Fixes double namespace introduced in #4148

leanprover-community-mathlib4-bot commented 2 weeks 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 770235855fd420e681f3a2c7ccac1cb1adede75d --onto 91244b2dd9d223006227648659203373f5a46b0b. (2024-05-14 19:36:45)