union
Lib.union : ''a list -> ''a list -> ''a list
Computes the union of two 'sets'.
If l1 and l2 are both 'sets' (lists with no repeated members),
union l1 l2 returns the set union of l1 and l2. In the case that
l1 or l2 is not a set, all the user can depend on is that
union l1 l2 returns a list l3 such that every unique element of l1
and l2 is in l3 and each element of l3 is found in either l1 or
l2.
Failure
Never fails.
Example
> union [1,2,3] [1,5,4,3];
val it = [2, 1, 5, 4, 3]: int list
> union [1,1,1] [1,2,3,2];
val it = [1, 2, 3, 2]: int list
> union [1,2,3,2] [1,1,1] ;
val it = [3, 2, 1, 1, 1]: int list
Comments
Do not make the assumption that the order of items in the list returned
by union is fixed. Later implementations may use different algorithms,
and return a different concrete result while still meeting the
specification.
A high-performance implementation of finite sets may be found in
structure HOLset.
ML equality types are used in the implementation of union and its kin.
This limits its applicability to types that allow equality. For other
types, typically abstract ones, use the 'op_' variants.
See also
Lib.op_union, Lib.U,
Lib.mk_set, Lib.mem,
Lib.insert, Lib.set_eq,
Lib.intersect, Lib.set_diff,
Lib.subtract