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