diff options
| author | Maxime Dénès | 2019-04-25 10:32:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-02 12:28:19 +0200 |
| commit | 016ed06128372e7b767efd4d3e1f71df9ca1e3d4 (patch) | |
| tree | 84a2c5c5a68ab9fefce2436e137cd608861b1c70 /clib/hMap.ml | |
| parent | ef0ef9f318a0af6542835b71ce7aaced021fff6d (diff) | |
Add union in Map interface
Diffstat (limited to 'clib/hMap.ml')
| -rw-r--r-- | clib/hMap.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/clib/hMap.ml b/clib/hMap.ml index 09ffb39c21..db59ef47b0 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -290,6 +290,14 @@ struct in Int.Map.merge fm s1 s2 + let union f s1 s2 = + let fm h m1 m2 = + let m = Map.union f m1 m2 in + if Map.is_empty m then None + else Some m + in + Int.Map.union fm s1 s2 + let compare f s1 s2 = let fc m1 m2 = Map.compare f m1 m2 in Int.Map.compare fc s1 s2 |