rename Recursion

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

diff --git a/Computation/Monad.v b/Computation/Monad.v
new file mode 100644 (file)
index 0000000..082a3dd
--- /dev/null
+++ b/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).