		Search-engine friendly clone of the ACL2 documentation.

Std/osets

Intersectp

(intersectp x y) checks whether X and Y have any common members.

Logically we just check whether the intersect of X and Y is empty.

In the execution, we use a faster function that checks for any common members and doesn't build any new sets.

Definitions and Theorems

Function: intersectp

(defun intersectp (x y)
       (declare (xargs :guard (and (setp x) (setp y))))
       (mbe :logic (not (empty (intersect x y)))
            :exec (fast-intersectp x y)))