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

@[simp]

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