aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/option.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/option.ml')
-rw-r--r--lib/option.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/option.ml b/lib/option.ml
index fbb883d30..f3047a3ca 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -188,4 +188,14 @@ module List =
|None -> find f t
|x -> x
+ let map f l =
+ let rec aux f l = match l with
+ | [] -> []
+ | x :: l ->
+ match f x with
+ | None -> raise Exit
+ | Some y -> y :: aux f l
+ in
+ try Some (aux f l) with Exit -> None
+
end