unionWith -package:Agda

The union with a combining function.

unionWith (++) (fromList [(5, "a"), (3, "b")]) (fromList [(5, "A"), (7, "C")]) == fromList [(3, "b"), (5, "aA"), (7, "C")]

Also see the performance note on fromListWith.

Union with a combining function.

unionWith (++) (fromList [(5, "a"), (3, "b")]) (fromList [(5, "A"), (7, "C")]) == fromList [(3, "b"), (5, "aA"), (7, "C")]

Also see the performance note on fromListWith.

The union with a combining function.

The union of two maps. If a key occurs in both maps, the provided function (first argument) will be used to compute the result.

The union with a combining function.

unionWith (++) (fromList [(5, "a"), (3, "b")]) (fromList [(5, "A"), (7, "C")]) == fromList [(3, "b"), (5, "aA"), (7, "C")]

The union of two maps. If a key occurs in both maps, the provided function (first argument) will be used to compute the result.

O(m*log(n/m + 1)), m <= n. Union with a combining function.

unionWith (++) (fromList [(5, "a"), (3, "b")]) (fromList [(5, "A"), (7, "C")]) == fromList [(3, "b"), (5, "aA"), (7, "C")]

Combine two maps. When a key exists in both maps, apply a function to both of the values and use the result of that as the value of the key in the resulting map.

Combine two Maps using a combining function for colliding keys

>>> unionWith (+) (fromList [("D",1),("C",2)]) (fromList [("B",3),("A",4)])
fromList [("D",1),("C",2),("B",3),("A",4)]

>>> unionWith (+) (fromList [("D",1),("C",2)]) (fromList [("C",3),("A",4)])
fromList [("D",1),("C",5),("A",4)]

forAllNonEmptyMap $ \xs -> forAllNonEmptyMap $ \ys -> Map.unionWith (++) (NonEmptyMap.flatten xs) (NonEmptyMap.flatten ys) == NonEmptyMap.flatten (NonEmptyMap.unionWith (++) xs ys)

The union of two maps. If a key occurs in both maps, the provided function (first argument) will be used to compute the result. Ordered traversal will go thru keys in the first map first.

Take the union of two tries, using a function to resolve conflicts. The resulting trie is constructed strictly, but the results of the combining function are evaluated lazily.

O(n+m).

Merge two event streams of the same type. The function argument specifies how event values are to be combined in case of a simultaneous occurrence. The semantics are

unionWith f ((timex,x):xs) ((timey,y):ys)
| timex <  timey = (timex,x)     : unionWith f xs ((timey,y):ys)
| timex >  timey = (timey,y)     : unionWith f ((timex,x):xs) ys
| timex == timey = (timex,f x y) : unionWith f xs ys

The union with a combining function.

O(m*log(n/m + 1)), m <= n. Union with a combining function.

unionWith (++) (fromList ((5, "a") :| [(3, "b")])) (fromList ((5, "A") :| [(7, "C")])) == fromList ((3, "b") :| [(5, "aA"), (7, "C")])

O(m*log(n/m + 1)), m <= n. Union with a combining function.

unionWith (++) (fromList ((5, "a") :| [(3, "b")])) (fromList ((5, "A") :| [(7, "C")])) == fromList ((3, "b") :| [(5, "aA"), (7, "C")])

Merge two unique maps, using the given combining funcion if a value with the same unique key exists in both maps.