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