mk_set
Lib.mk_set : ''a list -> ''a list
Transforms a list into one with distinct elements.
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.
See also
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