mathlib documentation

data.bitvec.basic

def bitvec.of_fin {n : } (i : fin (2 ^ n)) :

convert fin to bitvec

Equations
theorem bitvec.of_fin_val {n : } (i : fin (2 ^ n)) :
def bitvec.to_fin {n : } (i : bitvec n) :
fin (2 ^ n)

convert bitvec to fin

Equations
theorem bitvec.add_lsb_eq_twice_add_one {x : } {b : bool} :
bitvec.add_lsb x b = 2 * x + cond b 1 0
theorem bitvec.to_nat_lt {n : } (v : bitvec n) :
v.to_nat < 2 ^ n
theorem bitvec.add_lsb_div_two {x : } {b : bool} :
theorem bitvec.to_bool_add_lsb_mod_two {x : } {b : bool} :
to_bool (bitvec.add_lsb x b % 2 = 1) = b
theorem bitvec.of_nat_to_nat {n : } (v : bitvec n) :
theorem bitvec.to_fin_val {n : } (v : bitvec n) :
theorem bitvec.to_fin_le_to_fin_of_le {n : } {v₀ v₁ : bitvec n} (h : v₀ v₁) :
v₀.to_fin v₁.to_fin
theorem bitvec.of_fin_le_of_fin_of_le {n : } {i j : fin (2 ^ n)} (h : i j) :
theorem bitvec.to_fin_of_fin {n : } (i : fin (2 ^ n)) :
theorem bitvec.of_fin_to_fin {n : } (v : bitvec n) :