1 Require Export Computation.Monad.
2 Require Export Computation.Termination.
4 (* evaluate up to [n] computation steps *)
5 Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
12 match (bounded_eval _ n' c') with
14 | Some a => bounded_eval A n' (f a)
19 Inductive Unit : Set := unit : Unit.
22 * In theory we'd like to be able to do this (below), but it violates
23 * the Prop/Set separation:
25 * "Elimination of an inductive object of sort Prop is not allowed on a
26 * predicate in sort Set because proofs can be eliminated only to
30 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
32 | (Terminates_intro t') =>
39 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
40 match eval' c Unit (Return unit) (termination_is_safe A c t) with
44 Implicit Arguments eval [A].
45 Implicit Arguments bounded_eval [A].