mathlib documentation

data.bitvec.basic

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

convert fin to bitvec

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

def bitvec.to_fin {n : } :
bitvec nfin (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} :
v₀ v₁v₀.to_fin v₁.to_fin

theorem bitvec.of_fin_le_of_fin_of_le {n : } {i j : fin (2 ^ n)} :

theorem bitvec.to_fin_of_fin {n : } (i : fin (2 ^ n)) :

theorem bitvec.of_fin_to_fin {n : } (v : bitvec n) :