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