src/Computation/Monad.v

   1 Reserved Notation "# A" (at level 30).
   2 Section Constructors.
   3
   4   (** A co-inductive type representing a possibly-nonterminating computation *)
   5       CoInductive Computation (A:Set) : Type :=
   6
   7   (** terminate and return a value *)
   8        | Return  : A                               -> #A
   9
  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).
  16
  17 End Constructors.
  18
  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).
  23
  24 Notation "'call' c" :=
  25   (c >>= (fun x=>(Return x)))
  26   (at level 60, right associativity)
  27 .
  28
  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).