\DOC op_mk_set

\TYPE {op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list}

\SYNOPSIS
Transforms a list into one with elements that are distinct modulo
the supplied relation.

\KEYWORDS
list, set.

\DESCRIBE
An invocation {op_mk_set eq list} returns a list consisting of
the {eq}-distinct members of {list}. In particular, the result list
will not contain elements {x} and {y} at different positions such that
{eq x y} evaluates to {true}.

\FAILURE
If an application of {eq} fails when applied to two elements of {list}.

\EXAMPLE
{
- op_mk_set aconv [Term `\x y. x /\ y`,
                   Term `\y x. y /\ x`,
                   Term `\z a. z /\ a`];
> val it = [`\z a. z /\ a`] : term list
}


\COMMENTS
The order of items in the list returned by {op_mk_set}
is not dependable.

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

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

\SEEALSO
Lib.mk_set, Lib.op_mem, Lib.op_insert, Lib.op_union, Lib.op_U, Lib.op_intersect, Lib.op_set_diff.
\ENDDOC