Require Export Computation.Monad.
Require Export Computation.Termination.
-(* evaluate up to [n] computation steps *)
+(** evaluate up to [n] computation steps *)
Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
match n with
| O => None
end
end.
-Inductive Unit : Set := unit : Unit.
-
-(*
- * In theory we'd like to be able to do this (below), but it violates
- * the Prop/Set separation:
- *
- * "Elimination of an inductive object of sort Prop is not allowed on a
- * predicate in sort Set because proofs can be eliminated only to
- * build proofs."
+(** In theory we'd like to be able to do this (below), but it violates the Prop/Set separation.
*)
-(*
+(**
+<<
Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
match t with
| (Terminates_intro t') =>
| (ex_intro x y) => x
end
end.
-*)
+
+ "Elimination of an inductive object of sort Prop is not allowed on a
+ predicate in sort Set because proofs can be eliminated only to
+ build proofs."
+>>*)
+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
Implicit Arguments eval [A].
Implicit Arguments bounded_eval [A].
+