X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FMonad.v;fp=Computation%2FMonad.v;h=91df0c6b19cd5a79685512b2e186bc8dfb2c8148;hp=082a3dd2d8b0710184a41dbbb64cb105e0bc7faa;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d

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
--- 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].