### SET-DIFFERENCE$

elements of one list that are not elements of another
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

`(Set-difference$ l1 l2)`

equals a list that contains the `member`

s of
`l1`

that are not `member`

s of `l2`

. More precisely, the resulting
list is the same as one gets by deleting the members of `l2`

from `l1`

,
leaving the remaining elements in the same order as in `l1`

. 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 `set-difference$`

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
`set-difference$`

and its variants:

`(set-difference-eq l1 l2)`

is equivalent to
`(set-difference$ l1 l2 :test 'eq)`

;

`(set-difference-equal l1 l2)`

is equivalent to
`(set-difference$ l1 l2 :test 'equal)`

.

In particular, reasoning about any of these primitives reduces to reasoning
about the function `set-difference-equal`

.

`Set-difference$`

is similar to the Common Lisp primitive
`set-difference`

. However, Common Lisp does not specify the order of
elements in the result of a call of `set-difference`

.