Add Option.List.bind_list

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v
index 57cc52f06..2f6d8a2ce 100644
--- a/src/Util/OptionList.v
+++ b/src/Util/OptionList.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Notations.
 
 Module Option.
@@ -16,5 +17,17 @@ Module Option.
                end
            end.
     End map.
+
+    Fixpoint bind_list {A B} (v : list (option A)) (f : list A -> option B) : option B
+      := match v with
+         | nil => f nil
+         | x :: xs => (x <- x; @bind_list A B xs (fun xs => f (x :: xs)))
+         end%option%list.
+
+    Module Export Notations.
+      Notation "A <-- X ; B" := (bind_list X (fun A => B%option)) : option_scope.
+    End Notations.
   End List.
 End Option.
+
+Export Option.List.Notations.