aboutsummaryrefslogtreecommitdiff
path: root/clib
diff options
context:
space:
mode:
Diffstat (limited to 'clib')
-rw-r--r--clib/option.ml2
-rw-r--r--clib/option.mli3
2 files changed, 5 insertions, 0 deletions
diff --git a/clib/option.ml b/clib/option.ml
index c335e836c2..d1775ae3ae 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -55,6 +55,8 @@ let make x = Some x
(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
let bind x f = match x with Some y -> f y | None -> None
+let filter f x = bind x (fun v -> if f v then x else None)
+
(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
let init b x =
if b then
diff --git a/clib/option.mli b/clib/option.mli
index 4c5df30179..4672780cab 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -46,6 +46,9 @@ val make : 'a -> 'a option
(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
val bind : 'a option -> ('a -> 'b option) -> 'b option
+(** [filter f x] is [x] if [x] [Some y] and [f y] is true, [None] otherwise *)
+val filter : ('a -> bool) -> 'a option -> 'a option
+
(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
val init : bool -> 'a -> 'a option