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