Monads.v 741 Bytes
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
(* This file defines some helpful notations for the option monad. *)

3
Definition option_bind {A B : Type} (v : option A) (f : A -> option B) : option B :=
4
5
6
7
8
  match v with
  | Some val => f val
  | None => None
  end.

9
10
Notation "c >>= f" := (option_bind c f) (at level 50, left associativity).
Notation "f =<< c" := (option_bind c f) (at level 51, right associativity).
11

12
13
14
15
16
17
18
19
20
21
Notation "'do' x <- c1 ; c2" :=
  (option_bind c1 (fun x => c2))
    (at level 60, c1 at next level, right associativity).

Notation "'do' ' pat <- c1 ; c2" :=
  (option_bind c1 (fun x => match x with pat => c2 end))
    (at level 60, pat pattern, c1 at next level, right associativity).

Notation "'do' e1 ; e2" := (do _ <- e1 ; e2)
  (at level 60, right associativity).