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 members of l1 that are not members 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.