Major Section: ACL2-BUILT-INS
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.
