From c8cd6ec125ed7cd9b0b9518d195c1df4f4411115 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jun 2018 17:06:33 -0400 Subject: Add Option.List.bind_list --- src/Util/OptionList.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/Util/OptionList.v') 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. -- cgit v1.2.3