diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 5c59708211..c315ecd0ac 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -138,6 +138,9 @@ val list_join_map : ('a -> 'b list) -> 'a list -> 'b list val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list +(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) +val list_combinations : 'a list list -> 'a list list + (*s Arrays. *) |