@[simp]

theorem BitVec.toNat_pow {w : Nat} (b : BitVec w) (n : Nat) : (b ^ n).toNat = b.toNat ^ n % 2 ^ w

@[simp]

theorem BitVec.ofNat_pow (w x n : Nat) : BitVec.ofNat w (x ^ n) = BitVec.ofNat w x ^ n

@[simp]

theorem BitVec.toNat_ofFnLEAux {n : Nat} (m : Nat) (f : Fin n → Bool) : (ofFnLEAux m f).toNat = Nat.ofBits f % 2 ^ m

@[simp]

theorem BitVec.toFin_ofFnLEAux {n : Nat} (m : Nat) (f : Fin n → Bool) : (ofFnLEAux m f).toFin = Fin.ofNat (2 ^ m) (Nat.ofBits f)

@[simp]

theorem BitVec.toNat_ofFnLE {n : Nat} (f : Fin n → Bool) : (ofFnLE f).toNat = Nat.ofBits f

@[simp]

theorem BitVec.toFin_ofFnLE {n : Nat} (f : Fin n → Bool) : (ofFnLE f).toFin = Fin.ofBits f

@[simp]

theorem BitVec.toInt_ofFnLE {n : Nat} (f : Fin n → Bool) : (ofFnLE f).toInt = Int.ofBits f

theorem BitVec.getElem_ofFnLEAux {n m : Nat} (f : Fin n → Bool) (i : Nat) (h : i < n) (h' : i < m) : (ofFnLEAux m f)[i] = f ⟨i, h⟩

@[simp]

theorem BitVec.getElem_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Nat) (h : i < n) : (ofFnLE f)[i] = f ⟨i, h⟩

theorem BitVec.getLsb_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnLE f).getLsb i = f i

@[deprecated BitVec.getLsb_ofFnLE (since := "2025-06-17")]

theorem BitVec.getLsb'_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnLE f).getLsb i = f i

Alias of BitVec.getLsb_ofFnLE.

theorem BitVec.getLsbD_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Nat) : (ofFnLE f).getLsbD i = if h : i < n then f ⟨i, h⟩ else false

@[simp]

theorem BitVec.getMsb_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnLE f).getMsb i = f i.rev

@[deprecated BitVec.getMsb_ofFnLE (since := "2025-06-17")]

theorem BitVec.getMsb'_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnLE f).getMsb i = f i.rev

Alias of BitVec.getMsb_ofFnLE.

theorem BitVec.getMsbD_ofFnLE {n : Nat} (f : Fin n → Bool) (i : Nat) : (ofFnLE f).getMsbD i = if h : i < n then f ⟨i, h⟩.rev else false

theorem BitVec.msb_ofFnLE {n : Nat} (f : Fin n → Bool) : (ofFnLE f).msb = if h : n ≠ 0 then f ⟨n - 1, ⋯⟩ else false

@[simp]

theorem BitVec.toNat_ofFnBE {n : Nat} (f : Fin n → Bool) : (ofFnBE f).toNat = Nat.ofBits (f ∘ Fin.rev)

@[simp]

theorem BitVec.toFin_ofFnBE {n : Nat} (f : Fin n → Bool) : (ofFnBE f).toFin = Fin.ofBits (f ∘ Fin.rev)

@[simp]

theorem BitVec.toInt_ofFnBE {n : Nat} (f : Fin n → Bool) : (ofFnBE f).toInt = Int.ofBits (f ∘ Fin.rev)

@[simp]

theorem BitVec.getElem_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Nat) (h : i < n) : (ofFnBE f)[i] = f ⟨i, h⟩.rev

theorem BitVec.getLsb_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnBE f).getLsb i = f i.rev

@[deprecated BitVec.getLsb_ofFnBE (since := "2025-06-17")]

theorem BitVec.getLsb'_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnBE f).getLsb i = f i.rev

Alias of BitVec.getLsb_ofFnBE.

theorem BitVec.getLsbD_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Nat) : (ofFnBE f).getLsbD i = if h : i < n then f ⟨i, h⟩.rev else false

@[simp]

theorem BitVec.getMsb_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnBE f).getMsb i = f i

@[deprecated BitVec.getMsb_ofFnBE (since := "2025-06-17")]

theorem BitVec.getMsb'_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Fin n) : (ofFnBE f).getMsb i = f i

Alias of BitVec.getMsb_ofFnBE.

theorem BitVec.getMsbD_ofFnBE {n : Nat} (f : Fin n → Bool) (i : Nat) : (ofFnBE f).getMsbD i = if h : i < n then f ⟨i, h⟩ else false

theorem BitVec.msb_ofFnBE {n : Nat} (f : Fin n → Bool) : (ofFnBE f).msb = if h : n ≠ 0 then f ⟨0, ⋯⟩ else false