		Search-engine friendly clone of the ACL2 documentation.

Remove1-assoc

Remove the first pair with a given key from an association list

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

(Remove1-assoc key alist) returns an alist that is the same as the list alist, except that the first pair in alist with a car of key is deleted, if there is one; otherwise alist is returned. Note that the order of the elements of alist is unchanged (though one may be deleted).

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

The guard for a call of remove1-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 remove1-assoc and its variants:

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

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

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

Function: remove1-assoc-equal

(defun remove1-assoc-equal (key alist)
  (declare (xargs :guard (alistp alist)))
  (cond ((endp alist) nil)
        ((equal key (caar alist)) (cdr alist))
        (t (cons (car alist)
                 (remove1-assoc-equal key (cdr alist))))))