mk_set : ''a list -> ''a list
STRUCTURE
Lib
SYNOPSIS
Transforms a list into one with distinct elements.
DESCRIPTION
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
op_mk_set, mem, insert, union, U, set_diff, subtract, intersect, null_intersection, set_eq
HOL  Kananaskis-13