Set Implicit Arguments.
| Continuation support code |
Definition result := nat.
Definition withCont (A : Set) :=
(A -> result) -> result.
Definition withCont_const (A : Set) (v : A) : withCont A :=
fun f => f v.
Definition withCont_compose (A B : Set) (k1 : withCont A) (k2 : A -> withCont B) : withCont B :=
fun f => k1 (fun x => k2 x f).
Definition withCont_bind (A B : Set) (v : A) (f : A -> B) : B :=
f v.