better comments/documentation

[coinductive-monad.git] / Computation / Eval.v

diff --git a/Computation/Eval.v b/Computation/Eval.v
deleted file mode 100644 (file)
index 28a00a0..0000000
--- a/Computation/Eval.v
+++ /dev/null
@@ -1,45 +0,0 @@
-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.
-
-(*
- * 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."
- *)
-(*
-Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
-  match t with
-    | (Terminates_intro t') =>
-      match t' with
-        | (ex_intro x y) => x
-      end
-  end.
-*)
-
-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].