diff options
-rw-r--r-- | src/Util/OptionList.v | 13 |
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. |