op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
STRUCTURE
Lib
SYNOPSIS
Computes the union of two ‘sets’.
DESCRIPTION
If l1 and l2 are both ‘sets’ (lists with no repeated members), union eq l1 l2 returns the set union of l1 and l2, using eq as the implementation of element equality. If one or both of l1 and l2 have repeated elements, there may be repeated elements in the result.
FAILURE
If some application of eq fails.
EXAMPLE
- op_union (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [5,4,7];
> val it = [5, 4, 7] : int list

COMMENTS
Do not make the assumption that the order of items in the list returned by op_union is fixed. Later implementations may use different algorithms, and return a different concrete result while still meeting the specification.

There is no requirement that eq be recognizable as a kind of equality (it could be implemented by an order relation, for example).

A high-performance implementation of finite sets may be found in structure HOLset.

SEEALSO
union, op_mem, op_insert, op_mk_set, op_U, op_intersect, op_set_diff
HOL  Kananaskis-14