REMOVE-DUPLICATES

Major Section:  ACL2-BUILT-INS

General Forms:
(remove-duplicates x)
(remove-duplicates x :test 'eql)   ; same as above (eql as equality test)
(remove-duplicates x :test 'eq)    ; same, but eq is equality test
(remove-duplicates x :test 'equal) ; same, but equal is equality test

(Remove-duplicates x) returns the result of deleting duplicate elements from the beginning of the list or string x. For example, (remove-duplicates '(1 2 3 2 4)) is equal to '(1 3 2 4). The optional keyword, :TEST, has no effect logically, but provides the test (default eql) used for comparing x with successive elements of lst.

The guard for a call of remove-duplicates depends on the test. In all cases, the argument must satisfy stringp or true-listp. If the test is eql, then the argument must satisfy either stringp or eqlable-listp. If the test is eq, then the argument must satisfy symbol-listp.

The relation between remove-duplicates and its variants is related to the usual pattern for equality variants; see equality-variants. However, the possibility of a string argument changes the usual pattern a bit. As one might expect:

(remove-duplicates-eq lst) is equivalent to (remove-duplicates lst :test 'eq).

However, remove-duplicates-equal is defined without consideration of strings, for backward compatibility with versions of ACL2 through Version_4.2. The macro remove-duplicates-logic has been introduced to model the behavior of remove-duplicates even on strings; use :pe if you wish to see its definition. So we can say the following.

(remove-duplicates-logic lst) is equivalent to (remove-duplicates lst :test 'equal); and

(remove-duplicates-logic lst) is equal to (remove-duplicates-equal lst) when lst is not a string.

In particular, when the argument is not a string, reasoning about any of these primitives reduces to reasoning about the function remove-duplicates-equal.

Remove-duplicates is defined by Common Lisp. See any Common Lisp documentation for more information.