Test whether two lists intersect
(intersectp l1 l2)
(intersectp l1 l2 :test 'eql) ; same as above (eql as equality test)
(intersectp l1 l2 :test 'eq) ; same, but eq is equality test
(intersectp l1 l2 :test 'equal) ; same, but equal is equality test
(Intersectp l1 l2) returns t if l1 and l2 have a member in common, else it returns nil. The optional keyword,
:TEST, has no effect logically, but provides the test (default eql) used for comparing members of the two lists.
The guard for a call of intersectp depends on the test. In all
cases, both arguments must satisfy true-listp. If the test is eql, then one of the arguments must satisfy eqlable-listp. If the
test is eq, then one of the arguments must satisfy symbol-listp.
See equality-variants for a discussion of the relation between
intersectp and its variants:
(intersectp-eq x lst) is equivalent to (intersectp x
lst :test 'eq);
(intersectp-equal x lst) is equivalent to (intersectp x lst :test
In particular, reasoning about any of these primitives reduces to reasoning
about the function intersectp-equal.
(defun intersectp-equal (x y)
(declare (xargs :guard (and (true-listp x) (true-listp y))))
(cond ((endp x) nil)
((member-equal (car x) y) t)
(t (intersectp-equal (cdr x) y))))
- Lemmas about intersectp available in the std/lists
- (intersectp-witness x y) finds a some element that is a member
of both x and y, if one exists.
- Some theorems about the built-in function intersectp.