\DOC mk_set

\TYPE {mk_set : ''a list -> ''a list}

\SYNOPSIS
Transforms a list into one with distinct elements.

\KEYWORDS
list, set, eqtype.

\DESCRIBE
An invocation {mk_set list} returns a list consisting of the distinct
members of {list}. In particular, the result list has
no repeated elements.

\FAILURE
Never fails.

\EXAMPLE
{
- mk_set [1,1,1,2,2,2,3,3,4];
> val it = [1, 2, 3, 4] : int list
}


\COMMENTS
In some programming situations, it is convenient to implement sets
by lists, in which case {mk_set} may be helpful. However, such
an implementation is only suitable for small sets.

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

ML equality types are used in the implementation of {mk_set} and its kin.
This limits its applicability to types that allow equality. For other
types, typically abstract ones, use the `op_' variants.

\SEEALSO
Lib.op_mk_set, Lib.mem, Lib.insert, Lib.union, Lib.U, Lib.set_diff, Lib.subtract, Lib.intersect, Lib.null_intersection, Lib.set_eq.
\ENDDOC