Commit 2023-04-20 04:08 62057261

View on Github →

feat: port Data.Bitvec.Basic (#2179)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Bitvec/Basic.lean

added theorem Bitvec.addLsb_div_two

added theorem Bitvec.addLsb_eq_twice_add_one

added theorem Bitvec.decide_addLsb_mod_two

added def Bitvec.ofFin

added theorem Bitvec.ofFin_le_ofFin_of_le

added theorem Bitvec.ofFin_toFin

added theorem Bitvec.ofFin_val

added theorem Bitvec.ofNat_toNat

added def Bitvec.toFin

added theorem Bitvec.toFin_le_toFin_of_le

added theorem Bitvec.toFin_ofFin

added theorem Bitvec.toFin_val

added theorem Bitvec.toNat_eq_foldr_reverse

added theorem Bitvec.toNat_lt