null_intersection
Lib.null_intersection : ''a list -> ''a list -> bool
Tells if two lists have no common elements.
An invocation null_intersection l1 l2 is equivalent to
null(intersect l1 l2), but is more efficient in the case where the
intersection is not empty.
Failure
Never fails.
Example
> null_intersection [1,2,3,4] [5,6,7,8];
val it = true: bool
> null_intersection [1,2,3,4] [8,5,3];
val it = false: bool
Comments
A high-performance implementation of finite sets may be found in
structure HOLset.
See also
Lib.intersect, Lib.union,
Lib.U, Lib.mk_set, Lib.mem,
Lib.insert, Lib.set_eq,
Lib.set_diff