Major Section: ACL2-BUILT-INS
General Forms: (set-difference$ l1 l2) (set-difference$ l1 l2 :test 'eql) ; same as above (eql as equality test) (set-difference$ l1 l2 :test 'eq) ; same, but eq is equality test (set-difference$ 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 'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function intersectp-equal.
