Add the let* monadic notation

Inspired by the notation introduced by OCaml 4.08, we propose to
introduce a new notation following the same principle.

    let* x := p in q

is strictly equivalent to

    x <- p;; q

The former can be made available by importing the newly introduced
[MonadLetNotation]. Loading this module does not provide the
arrow-based notation, which can still be made available by importing
the [MonadNotation] module as before.

Author: lthms

examples/Notations.v

@@ -0,0 +1,30 @@
+Require Import ExtLib.Structures.Monad.
+Generalizable All Variables.
+
+Module NotationExample.
+
+  Import MonadNotation.
+  Open Scope monad_scope.
+
+  Fixpoint repeatM `{Monad M} (n : nat) `(x : A) (p : A -> M A) : M unit :=
+    match n with
+    | O => ret tt
+    | S n => y <- p x;;
+             repeatM n y p
+    end.
+
+End NotationExample.
+
+Module LetNotationExample.
+
+  Import MonadLetNotation.
+  Open Scope monad_scope.
+
+  Fixpoint repeatM `{Monad M} (n : nat) `(x : A) (p : A -> M A) : M unit :=
+    match n with
+    | O => ret tt
+    | S n => let* y := p x in
+             repeatM n y p
+    end.
+
+End LetNotationExample.

examples/_CoqProject

@@ -7,3 +7,4 @@ MonadReasoning.v
 Printing.v
 UsingSets.v
 WithDemo.v
+Notations.v

theories/Structures/Monad.v

@@ -49,29 +49,47 @@ Section monadic.
 
 End monadic.
 
-Module MonadNotation.
+Module MonadBaseNotation.
 
   Delimit Scope monad_scope with monad.
 
   Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 58, left associativity) : monad_scope.
   Notation "f =<< c" := (@bind _ _ _ _ c f) (at level 61, right associativity) : monad_scope.
   Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope.
 
+  Notation "e1 ;; e2" := (@bind _ _ _ _ e1%monad (fun _ => e2%monad))%monad
+    (at level 61, right associativity) : monad_scope.
+
+End MonadBaseNotation.
+
+Module MonadNotation.
+
+  Export MonadBaseNotation.
+
   Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2))
     (at level 61, c1 at next level, right associativity) : monad_scope.
 
   Notation "` x : t <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x : t => c2))
     (at level 61, t at next level, c1 at next level, x ident, right associativity) : monad_scope.
 
-  Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad
-    (at level 61, right associativity) : monad_scope.
-
   Notation "' pat <- c1 ;; c2" :=
     (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))
     (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope.
 
 End MonadNotation.
 
+Module MonadLetNotation.
+
+  Export MonadBaseNotation.
+
+  Notation "'let*' x ':=' c1 'in' c2" := (@bind _ _ _ _ c1 (fun x => c2))
+    (at level 61, c1 at next level, right associativity) : monad_scope.
+
+  Notation "'`let*' x ':' t ':=' c1 'in' c2" := (@bind _ _ _ _ c1 (fun x : t => c2))
+    (at level 61, t at next level, c1 at next level, x ident, right associativity) : monad_scope.
+
+End MonadLetNotation.
+
 Section Instances.
 
 Universe d c.