Add do notation for option

1 files changed, 11 insertions, 0 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 666d740..47360d6 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -65,6 +65,17 @@ Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : o
   | _ => None
   end.
 
+Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
+  match f with
+  | Some a => g a
+  | _ => None
+  end.
+
+Module Notation.
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+   (at level 200, X ident, A at level 100, B at level 200).
+End Notation.
+
 End Option.
 
 Parameter debug_print : string -> unit.