better comments/documentation

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

diff --git a/Computation/Eval.v b/src/Computation/Eval.v
similarity index 73%
rename from Computation/Eval.v
rename to src/Computation/Eval.v
index 28a00a0..7693483 100644 (file)
--- a/Computation/Eval.v
+++ b/src/Computation/Eval.v
@@ -1,7 +1,7 @@
 Require Export Computation.Monad.
 Require Export Computation.Termination.
 
 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
 Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
   match n with
     | O      => None

@@ -16,17 +16,10 @@ Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
       end
   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."
+(** 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') =>
 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
   match t with
     | (Terminates_intro t') =>

@@ -34,8 +27,13 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
         | (ex_intro x y) => x
       end
   end.
         | (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
 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

@@ -43,3 +41,4 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
 
 Implicit Arguments eval [A].
 Implicit Arguments bounded_eval [A].
 
 Implicit Arguments eval [A].
 Implicit Arguments bounded_eval [A].

+