		Search-engine friendly clone of the ACL2 documentation.

Remove-assoc

Remove all pairs with a given key from an association list

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

(Remove-assoc key alist) returns an alist that is the same as the list alist, except that all pairs in alist with a car of key are deleted (if any; otherwise alist is returned). Note that the order of the elements of alist is unchanged (though some may be deleted).

Also see remove1-assoc for a similar utility that deletes only the first pair in an alist with a given key, rather than all such pairs.

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

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

(remove-assoc-eq key alist) is equivalent to (remove-assoc key alist :test 'eq);

(remove-assoc-equal key alist) is equivalent to (remove-assoc key alist :test 'equal).

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

Function: remove-assoc-equal

(defun remove-assoc-equal (x alist)
  (declare (xargs :guard (alistp alist)))
  (cond ((endp alist) nil)
        ((equal x (car (car alist)))
         (remove-assoc-equal x (cdr alist)))
        (t (cons (car alist)
                 (remove-assoc-equal x (cdr alist))))))

Subtopics

Std/alists/remove-assoc-equal: Theorems about remove-assoc-equal in the std/alists library.