Require Export Computation.Monad. Require Export Computation.Termination. (* evaluate up to [n] computation steps *) Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A := match n with | O => None | (S n') => match c with | Return b => Some b | Bind _ f c' => match (bounded_eval _ n' c') with | None => None | Some a => bounded_eval A n' (f a) end end end. Inductive Unit : Set := unit : Unit. Definition eval (A:Set) (c:#A) (t:Terminates c) : A := match eval' c Unit (Return unit) (termination_is_safe A c t) with | exist x pf => x end. Implicit Arguments eval [A]. Implicit Arguments bounded_eval [A].