X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=Computation%2FEval.v;fp=Computation%2FEval.v;h=0000000000000000000000000000000000000000;hp=28a00a03129f6c35e96ccac2541b8b184c90efb8;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d

diff --git a/Computation/Eval.v b/Computation/Eval.v
deleted file mode 100644
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].