+++ /dev/null
-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).