better comments/documentation

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

diff --git a/Computation/Monad.v b/src/Computation/Monad.v
similarity index 79%
rename from Computation/Monad.v
rename to src/Computation/Monad.v
index 082a3dd..91df0c6 100644 (file)
--- a/Computation/Monad.v
+++ b/src/Computation/Monad.v
@@ -1,13 +1,13 @@
 Reserved Notation "# A" (at level 30).
 Section Constructors.
 
-  (* a co-inductive type representing a possibly-nonterminating computation *)
-     CoInductive Computation (A:Set) : Type :=
+  (** A co-inductive type representing a possibly-nonterminating computation *)
+      CoInductive Computation (A:Set) : Type :=
 
-  (* terminate and return a value *)
+  (** terminate and return a value *)
        | Return  : A                               -> #A
          
-  (* monadic >>= (bind) operator *)
+  (** monadic >>= (bind) operator *)
        | Bind    : forall (B:Set),  (B->#A) ->  #B -> #A
          where "# A" := (Computation A).
      Implicit Arguments Return [A].