Add Option.{lift,map,combine}, List.Option.lift

These will be useful for extending the AST with `option` types.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v
index c2157346e..4b88dd9a3 100644
--- a/src/Util/OptionList.v
+++ b/src/Util/OptionList.v
@@ -25,6 +25,11 @@ Module Option.
          | x :: xs => (x <- x; @bind_list A B xs (fun xs => f (x :: xs)))
          end%option%list.
 
+    Definition lift {A} (ls : list (option A)) : option (list A)
+      := fold_right (fun x xs => x <- x; xs <- xs; Some (x :: xs))%option
+                    (Some nil)
+                    ls.
+
     Module Export Notations.
       Notation "A <-- X ; B" := (bind_list X (fun A => B%option)) : option_scope.
     End Notations.