		Search-engine friendly clone of the ACL2 documentation.

No-duplicatesp

Check for duplicates in a list

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

(no-duplicatesp lst) is true if and only if no member of lst occurs twice in lst. The optional keyword, :TEST, has no effect logically, but provides the test (default eql) used for comparing elements of lst.

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

See equality-variants for a discussion of the relation between no-duplicatesp and its variants:

(no-duplicatesp-eq x lst) is equivalent to (no-duplicatesp x lst :test 'eq);

(no-duplicatesp-equal x lst) is equivalent to (no-duplicatesp x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function no-duplicatesp-equal.

Function: no-duplicatesp-equal

(defun no-duplicatesp-equal (l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) t)
        ((member-equal (car l) (cdr l)) nil)
        (t (no-duplicatesp-equal (cdr l)))))

Subtopics

Duplicity: (duplicity a x) counts how many times the element a occurs within the list x.
Uniquep: Sometimes better than no-duplicatesp: first sorts the list and then looks for adjacent duplicates.