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

diff --git a/src/Computation/Monad.v b/src/Computation/Monad.v
new file mode 100644
index 0000000..91df0c6
--- /dev/null
+++ b/src/Computation/Monad.v
@@ -0,0 +1,32 @@
+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).