Fixed-length bit strings and Boolean functions

A bit string is indexed by its coordinates, so selecting or updating one bit uses the usual functions on Fin n → Bool.

@[reducible, inline]

abbrev Cslib.BitString (n : ℕ) : Type

A string of n bits, indexed by its coordinates.

Equations

• Cslib.BitString n = (Fin n → Bool)

@[reducible, inline]

abbrev Cslib.BooleanFunction (n : ℕ) : Type

A Boolean function of n input bits.

Equations

• Cslib.BooleanFunction n = (Cslib.BitString n → Bool)