aboutsummaryrefslogtreecommitdiffhomepage
path: root/clib
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-21 21:18:49 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 21:58:31 +0100
commit61c9bd4bc14d3479a98c2b53adf1b86fa84f13bf (patch)
tree50b4e7585ac5e3b22466208fd9d88632625fa4c4 /clib
parentbfb393596b1df815a109c9c600b9a2b413561fcb (diff)
Add function bind in option.ml.
Diffstat (limited to 'clib')
-rw-r--r--clib/option.ml3
-rw-r--r--clib/option.mli3
2 files changed, 6 insertions, 0 deletions
diff --git a/clib/option.ml b/clib/option.ml
index 21913e8f7..32fe2fc5f 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -52,6 +52,9 @@ let get = function
(** [make x] returns [Some x]. *)
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
+
(** [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 226099352..67b42268a 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -43,6 +43,9 @@ val get : 'a option -> 'a
(** [make x] returns [Some x]. *)
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
+
(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
val init : bool -> 'a -> 'a option