mk_set : ''a list -> ''a list
- mk_set [1,1,1,2,2,2,3,3,4]; > val it = [1, 2, 3, 4] : int list
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.