Encodings of Booleans, signs and the unit type

Turing.MultiTapeTM.encBool encodes a Boolean by one symbol, Turing.MultiTapeTM.encSign a sign, such as a head move, by at most one symbol, and Turing.MultiTapeTM.encUnit the unit by the empty word.

def Turing.MultiTapeTM.encBool : Bool ↪ List Bool

The encoding b ↦ [b] of Bool.

@[simp]

theorem Turing.MultiTapeTM.encBool_apply (b : Bool) : encBool b = [b]

def Turing.MultiTapeTM.encSign : SignType ↪ List Bool

Signs: 0 ↦ [], -1 ↦ [false] and 1 ↦ [true].

def Turing.MultiTapeTM.encUnit : Unit ↪ List Bool

The unit type, encoded by the empty word.

@[simp]

theorem Turing.MultiTapeTM.encUnit_apply (u : Unit) : encUnit u = []