1\DOC set_eq
2
3\TYPE {set_eq : ''a list -> ''a list -> bool}
4
5\SYNOPSIS
6Tells whether two lists have the same elements.
7
8\KEYWORDS
9set, list, eqtype.
10
11\DESCRIBE
12An application {set_eq l1 l2} returns {true} just in case {l1} and {l2}
13are permutations of each other when duplicate elements within each list
14are ignored.
15
16\FAILURE
17Never fails.
18
19\EXAMPLE
20{
21- set_eq [1,2,1] [1,2,2,1];
22> val it = true : bool
23
24- set_eq [1,2,1] [2,1];
25> val it = true : bool
26}
27
28
29\COMMENTS
30A high-performance implementation of finite sets may be found in
31structure {HOLset}.
32
33ML equality types are used in the implementation of {set_eq}
34and its kin. This limits its applicability to types that
35allow equality. For other types, typically abstract ones,
36use the `op_' variants.
37
38\SEEALSO
39Lib.intersect, Lib.union, Lib.U, Lib.mk_set, Lib.mem, Lib.insert, Lib.set_diff.
40
41\ENDDOC
42