1\DOC op_set_diff 2 3\TYPE {op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list} 4 5\SYNOPSIS 6Computes the set-theoretic difference of two `sets', modulo a 7supplied relation. 8 9\KEYWORDS 10list, set. 11 12\DESCRIBE 13{op_set_diff eq l1 l2} returns a list consisting of those elements 14of {l1} that are not {eq} to some element of {l2}. 15 16\FAILURE 17Fails if an application of {eq} fails. 18 19\EXAMPLE 20{ 21- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [4,5,6]; 22> val it = [] : int list 23 24- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [2,4,6,8]; 25> val it = [1, 3] : int list 26} 27 28 29\COMMENTS 30The order in which the elements occur in the resulting list should 31not be depended upon. 32 33A high-performance implementation of finite sets may be found in 34structure {HOLset}. 35 36\SEEALSO 37Lib.set_diff, Lib.op_mem, Lib.op_insert, Lib.op_union, Lib.op_U, Lib.op_mk_set, Lib.op_intersect. 38\ENDDOC 39