Add Option.List.map

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Util/Option.v b/src/Util/Option.v
index b9e64910c..e14ad263e 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -18,6 +18,23 @@ Module Export Notations.
 End Notations.
 Local Open Scope option_scope.
 
+Module List.
+  Section map.
+    Context {A B}
+            (f : A -> option B).
+
+    Fixpoint map (ls : list A) : list B
+      := match ls with
+         | nil => nil
+         | cons x xs
+           => match f x with
+              | Some fx => fx :: map xs
+              | None => map xs
+              end
+         end.
+  End map.
+End List.
+
 Section Relations.
   Definition option_eq {A} eq (x y : option A) :=
     match x with