better comments/documentation

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

diff --git a/Computation/Monad.v b/Computation/Monad.v
deleted file mode 100644 (file)
index 082a3dd..0000000
--- a/Computation/Monad.v
+++ /dev/null
@@ -1,32 +0,0 @@
-Reserved Notation "# A" (at level 30).
-Section Constructors.
-
-  (* a co-inductive type representing a possibly-nonterminating computation *)
-     CoInductive Computation (A:Set) : Type :=
-
-  (* terminate and return a value *)
-       | Return  : A                               -> #A
-         
-  (* monadic >>= (bind) operator *)
-       | Bind    : forall (B:Set),  (B->#A) ->  #B -> #A
-         where "# A" := (Computation A).
-     Implicit Arguments Return [A].
-     Implicit Arguments Bind [A B].
-     Notation "c >>= f" := (Bind f c) (at level 20).
-     
-End Constructors.
-
-Notation "# A" := (Computation A).
-Implicit Arguments Return [A].
-Implicit Arguments Bind [A B].
-Notation "c >>= f" := (Bind f c) (at level 20).
-
-Notation "'call' c" :=
-  (c >>= (fun x=>(Return x)))
-  (at level 60, right associativity)
-.
-
-Notation "var <- c ; rest" := 
-  (* I need this "fun" to tell the parser that "var" is bound *)
-  (c >>= (fun var => rest))
-  (at level 60, right associativity).