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.

Estimated changes

deleted def BitVec.adc'
deleted def BitVec.addLsb
deleted def BitVec.getLsb'
deleted def BitVec.getMsb'
deleted def BitVec.sbb
deleted def BitVec.toBEList
deleted def BitVec.toLEList
deleted theorem BitVec.addLsb_div_two
deleted theorem BitVec.extractLsb_eq
deleted theorem BitVec.ofFin_and
deleted theorem BitVec.ofFin_mul
deleted theorem BitVec.ofFin_natCast
deleted theorem BitVec.ofFin_neg
deleted theorem BitVec.ofFin_nsmul
deleted theorem BitVec.ofFin_ofNat
deleted theorem BitVec.ofFin_one
deleted theorem BitVec.ofFin_or
deleted theorem BitVec.ofFin_pow
deleted theorem BitVec.ofFin_toFin
deleted theorem BitVec.ofFin_val
deleted theorem BitVec.ofFin_xor
deleted theorem BitVec.ofFin_zero
deleted theorem BitVec.ofFin_zsmul
deleted theorem BitVec.ofNat_toNat'
deleted theorem BitVec.ofNat_toNat_of_eq
deleted theorem BitVec.toFin_inj
deleted theorem BitVec.toFin_injective
deleted theorem BitVec.toFin_natCast
deleted theorem BitVec.toFin_neg
deleted theorem BitVec.toFin_nsmul
deleted theorem BitVec.toFin_ofFin
deleted theorem BitVec.toFin_one
deleted theorem BitVec.toFin_pow
deleted theorem BitVec.toFin_val
deleted theorem BitVec.toFin_zero
deleted theorem BitVec.toFin_zsmul
deleted theorem BitVec.toNat_extractLsb'
deleted theorem BitVec.toNat_inj
deleted theorem BitVec.toNat_injective
deleted theorem BitVec.toNat_lt_toNat
deleted theorem BitVec.toNat_ofNat_of_lt