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).