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

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