1\DOC
2
3\TYPE {op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list}
4
5\SYNOPSIS
6Computes the union of two `sets'.
7
8\KEYWORDS
9list, set.
10
11\DESCRIBE
12If {l1} and {l2} are both `sets' (lists with no repeated members),
13{union eq l1 l2} returns the set union of {l1} and {l2}, using {eq} as the
14implementation of element equality. If one or both of {l1} and {l2} have
15repeated elements, there may be repeated elements in the result.
16
17\FAILURE
18If some application of {eq} fails.
19
20\EXAMPLE
21{
22- op_union (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [5,4,7];
23> val it = [5, 4, 7] : int list
24}
25
26
27\COMMENTS
28Do not make the assumption that the order of items in the list
29returned by {op_union} is fixed. Later implementations may use
30different algorithms, and return a different concrete result
31while still meeting the specification.
32
33There is no requirement that {eq} be recognizable as a kind of
34equality (it could be implemented by an order relation, for example).
35
36A high-performance implementation of finite sets may be found in
37structure {HOLset}.
38
39\SEEALSO
40Lib.union, Lib.op_mem, Lib.op_insert, Lib.op_mk_set, Lib.op_U, Lib.op_intersect, Lib.op_set_diff.
41\ENDDOC
42