The encoding of options

encOption enc encodes none as the empty word and some a as true followed by enc a. It has the capabilities of Turing.MultiTapeTM.OptionEncoding.

Main definitions

• Turing.MultiTapeTM.encOption: the encoding of options.

def Turing.MultiTapeTM.encOption {α : Type u} (enc : α ↪ List Bool) : Option α ↪ List Bool

Options encoded with none as the empty word and some a as true followed by enc a.

@[simp]

theorem Turing.MultiTapeTM.encOption_none {α : Type u} {enc : α ↪ List Bool} : (encOption enc) none = []

@[simp]

theorem Turing.MultiTapeTM.encOption_some {α : Type u} {enc : α ↪ List Bool} (a : α) : (encOption enc) (some a) = true :: enc a

instance Turing.MultiTapeTM.instOptionEncodingEncOption {α : Type u} {enc : α ↪ List Bool} : OptionEncoding enc (encOption enc)