Remove-duplicates
Remove duplicates from a string or a list
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.
Function: remove-duplicates-equal
(defun remove-duplicates-equal (l)
(declare (xargs :guard (true-listp l)))
(cond ((endp l) nil)
((member-equal (car l) (cdr l))
(remove-duplicates-equal (cdr l)))
(t (cons-with-hint (car l)
(remove-duplicates-equal (cdr l))
l))))
Remove-duplicates is defined by Common Lisp. See any Common Lisp
documentation for more information.
Subtopics
- Nat-list-remove-duplicates
- High-performance duplicate-removal function for nat-listps.
- Hons-remove-duplicates
- (hons-remove-duplicates l) removes duplicate elements from a
list, and is implemented using fast-alists.
- Std/lists/remove-duplicates-equal
- Lemmas about remove-duplicates-equal available in the std/lists library.
