diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/option.ml | 8 | ||||
| -rw-r--r-- | lib/option.mli | 6 |
2 files changed, 14 insertions, 0 deletions
diff --git a/lib/option.ml b/lib/option.ml index abdae892f2..35f9bd7d1e 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -64,6 +64,14 @@ let flatten = function | _ -> None +(** [append x y] is the first element of the concatenation of [x] and + [y] seen as lists. *) +let append o1 o2 = + match o1 with + | Some _ -> o1 + | None -> o2 + + (** {6 "Iterators"} ***) (** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing diff --git a/lib/option.mli b/lib/option.mli index af8696a5e4..e9d76572e3 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -47,6 +47,12 @@ val init : bool -> 'a -> 'a option (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) val flatten : 'a option option -> 'a option +(** [append x y] is the first element of the concatenation of [x] and + [y] seen as lists. In other words, [append (Some a) y] is [Some + a], [append None (Some b)] is [Some b], and [append None None] is + [None]. *) +val append : 'a option -> 'a option -> 'a option + (** {6 "Iterators"} ***) |
