		Search-engine friendly clone of the ACL2 documentation.

Remove1

Remove first occurrences, testing using eql

General Forms:
(remove1 x lst)
(remove1 x lst :test 'eql)   ; same as above (eql as equality test)
(remove1 x lst :test 'eq)    ; same, but eq is equality test
(remove1 x lst :test 'equal) ; same, but equal is equality test

(Remove1 x lst) is equal to lst if x is not a member of lst, else is the result of removing the first occurrences of x from lst. The optional keyword, :TEST, has no effect logically, but provides the test (default eql) used for comparing x with successive elements of lst.

Also see remove.

The guard for a call of remove1 depends on the test. In all cases, the second argument must satisfy true-listp. If the test is eql, then either the first argument must be suitable for eql (see eqlablep) or the second argument must satisfy eqlable-listp. If the test is eq, then either the first argument must be a symbol or the second argument must satisfy symbol-listp.

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

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

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

Function: remove1-equal

(defun remove1-equal (x l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
        ((equal x (car l)) (cdr l))
        (t (cons-with-hint (car l)
                           (remove1-equal x (cdr l))
                           l))))

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

Subtopics

Std/lists/remove1-equal: Lemmas about remove1 available in the std/lists library.