1\DOC mk_set
2
3\TYPE {mk_set : ''a list -> ''a list}
4
5\SYNOPSIS
6Transforms a list into one with distinct elements.
7
8\KEYWORDS
9list, set, eqtype.
10
11\DESCRIBE
12An invocation {mk_set list} returns a list consisting of the distinct
13members of {list}. In particular, the result list has
14no repeated elements.
15
16\FAILURE
17Never fails.
18
19\EXAMPLE
20{
21- mk_set [1,1,1,2,2,2,3,3,4];
22> val it = [1, 2, 3, 4] : int list
23}
24
25
26\COMMENTS
27In some programming situations, it is convenient to implement sets
28by lists, in which case {mk_set} may be helpful. However, such
29an implementation is only suitable for small sets.
30
31A high-performance implementation of finite sets may be found in
32structure {HOLset}.
33
34ML equality types are used in the implementation of {mk_set} and its kin.
35This limits its applicability to types that allow equality. For other
36types, typically abstract ones, use the `op_' variants.
37
38\SEEALSO
39Lib.op_mk_set, Lib.mem, Lib.insert, Lib.union, Lib.U, Lib.set_diff, Lib.subtract, Lib.intersect, Lib.null_intersection, Lib.set_eq.
40\ENDDOC
41