diff options
Diffstat (limited to 'lib/option.ml')
-rw-r--r-- | lib/option.ml | 10 |
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 |