		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 emptyp.

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 (emptyp (intersect x y)))
       :exec (fast-intersectp x y)))