@[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

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

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

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

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