Theorems · Definition · logic and foundations

Turing.ListBlank

(Γ : Type u_1) → [Inhabited Γ] → Type u_1

A ListBlank Γ is a quotient of List Γ by extension by blanks at the end. This is used to represent half-tapes of a Turing machine, so that we can pretend that the list continues infinitely with blanks.

Defined in

Mathlib.Computability.TuringMachine.Tape

Cited by

68 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Inhabited