The single-symbol encoding of Booleans

def Turing.MultiTapeTM.encBool : Bool ↪ List Bool

The encoding b ↦ [b] of Bool.

@[simp]

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