Description
mergePairs(x,y,f) merges sorted lists of pairs.
It merges
x and
y, which should be lists of pairs
(k,v) arranged in increasing order according to the key
k. The result will be a list of pairs, also arranged in increasing order, each of which is either from
x or from
y, or in the case where a key
k occurs in both, with say
(k,v) in
x and
(k,w) in
y, then the result will contain the pair
(k,f(v,w)). Thus the function
f is used for combining the values when the keys collide. The class of the result is taken to be the minimal common ancestor of the class of
x and the class of
y.