1\DOC null_intersection 2 3\TYPE {null_intersection : ''a list -> ''a list -> bool} 4 5\SYNOPSIS 6Tells if two lists have no common elements. 7 8\KEYWORDS 9set, list, eqtype. 10 11\DESCRIBE 12An invocation {null_intersection l1 l2} is equivalent to 13{null(intersect l1 l2)}, but is more efficient in the case where 14the intersection is not empty. 15 16\FAILURE 17Never fails. 18 19\EXAMPLE 20{ 21- null_intersection [1,2,3,4] [5,6,7,8]; 22> val it = true : bool 23 24- null_intersection [1,2,3,4] [8,5,3]; 25> val it = false : bool 26} 27 28 29\COMMENTS 30A high-performance implementation of finite sets may be found in 31structure {HOLset}. 32 33\SEEALSO 34Lib.intersect, Lib.union, Lib.U, Lib.mk_set, Lib.mem, Lib.insert, Lib.set_eq, Lib.set_diff. 35\ENDDOC 36