@[reducible, inline]

abbrev Fin.ofBits {n : Nat} (f : Fin n → Bool) : Fin (2 ^ n)

Construct an element of Fin (2 ^ n) from a sequence of bits (little endian).

Equations

• Fin.ofBits f = ⟨Nat.ofBits f, ⋯⟩

@[simp]

theorem Fin.val_ofBits {n : Nat} (f : Fin n → Bool) : ↑(Fin.ofBits f) = Nat.ofBits f