diff options
Diffstat (limited to 'src/util.mli')
| -rw-r--r-- | src/util.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/util.mli b/src/util.mli index 11588de2..a7818f93 100644 --- a/src/util.mli +++ b/src/util.mli @@ -90,6 +90,10 @@ val option_binop : ('a -> 'a -> 'a) -> 'a option -> 'a option -> 'a option whereas [option_get_exn exn (Some x)] returns [x]. *) val option_get_exn : exn -> 'a option -> 'a +(** [option_these xs] extracts the elements of the list [xs] + wrapped in [Some]. *) +val option_these : 'a option list -> 'a list + (** [changed2 f g x h y] applies [g] to [x] and [h] to [y]. If both function applications return [None], then [None] is returned. Otherwise [f] is applied to the results. For this |