--- /dev/null
+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].