From 007b01bcae6abcc88dbcd540d024cdf3df6a603b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 15 Apr 2020 17:30:01 +0100
Subject: Add do notation for option

---
 src/common/Coquplib.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src')

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.
-- 
cgit