ivg

(*** Turing Machines in Coq *)

(** Some preliminary types we'll use *)
CoInductive CoList (A: Type) := CONS (a:A) (t:CoList A) | NIL.

Arguments CONS [A] _ _.
Arguments NIL [A].

CoInductive Delay A := HERE (a:A) | LATER (_:Delay A).