Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-25 09:35
90388168
View on Github →
feat: port data.bitvec.core (
#1731
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Bitvec/Core.lean
added
def
Bitvec.Sge
added
def
Bitvec.Sgt
added
def
Bitvec.Sle
added
def
Bitvec.Slt
added
def
Bitvec.Uge
added
def
Bitvec.Ugt
added
def
Bitvec.Ule
added
def
Bitvec.Ult
added
def
Bitvec.adc
added
def
Bitvec.addLsb
added
def
Bitvec.append
added
def
Bitvec.bitsToNat
added
theorem
Bitvec.bitsToNat_toList
added
theorem
Bitvec.bits_toNat_decide
added
def
Bitvec.fillShr
added
theorem
Bitvec.ofNat_succ
added
def
Bitvec.sbb
added
def
Bitvec.sborrow
added
def
Bitvec.shl
added
def
Bitvec.sshr
added
theorem
Bitvec.toNat_append
added
theorem
Bitvec.toNat_ofNat
added
def
Bitvec.uborrow
added
def
Bitvec.ushr
added
def
Bitvec
Modified
Mathlib/Init/Data/Nat/Lemmas.lean
added
theorem
Nat.cond_decide_mod_two