Reserved Notation "# A" (at level 30).
Section Constructors.
- (* a co-inductive type representing a possibly-nonterminating computation *)
- CoInductive Computation (A:Set) : Type :=
+ (** A co-inductive type representing a possibly-nonterminating computation *)
+ CoInductive Computation (A:Set) : Type :=
- (* terminate and return a value *)
+ (** terminate and return a value *)
| Return : A -> #A
- (* monadic >>= (bind) operator *)
+ (** monadic >>= (bind) operator *)
| Bind : forall (B:Set), (B->#A) -> #B -> #A
where "# A" := (Computation A).
Implicit Arguments Return [A].