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`

.