Commit 2024-05-31 15:10 daa801e2
View on Github →chore: remove most of the material on BitVec (#13286) This PR removes most of the material on BitVec. While it is being actively developed in Lean, we do not want conflicting, but essentially unused, material here causing conflicts. If downstream users of Mathlib find that they need some of this material is being used, they are advised to either:
- restore the material in their downstream repository
- ask someone from the FRO, e.g. @semorrison, about making a PR adding it to the Lean library.