1 Reserved Notation "# A" (at level 30).
4 (** A co-inductive type representing a possibly-nonterminating computation *)
5 CoInductive Computation (A:Set) : Type :=
7 (** terminate and return a value *)
10 (** monadic >>= (bind) operator *)
11 | Bind : forall (B:Set), (B->#A) -> #B -> #A
12 where "# A" := (Computation A).
13 Implicit Arguments Return [A].
14 Implicit Arguments Bind [A B].
15 Notation "c >>= f" := (Bind f c) (at level 20).
19 Notation "# A" := (Computation A).
20 Implicit Arguments Return [A].
21 Implicit Arguments Bind [A B].
22 Notation "c >>= f" := (Bind f c) (at level 20).
24 Notation "'call' c" :=
25 (c >>= (fun x=>(Return x)))
26 (at level 60, right associativity)
29 Notation "var <- c ; rest" :=
30 (* I need this "fun" to tell the parser that "var" is bound *)
31 (c >>= (fun var => rest))
32 (at level 60, right associativity).