		Search-engine friendly clone of the ACL2 documentation.

Put-assoc

Modify an association list by associating a value with a key

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

(Put-assoc name val alist) returns an alist that is the same as the list alist, except that the first pair in alist with a car of name is replaced by (cons name val), if there is one. If there is no such pair, then (cons name val) is added at the end. Note that the order of the keys occurring in alist is unchanged (though a new key may be added).

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

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

(put-assoc-eq name val alist) is equivalent to (put-assoc name val alist :test 'eq);

(put-assoc-equal name val alist) is equivalent to (put-assoc name val alist :test 'equal).

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

Function: put-assoc-equal

(defun put-assoc-equal (name val alist)
  (declare (xargs :guard (alistp alist)))
  (cond ((endp alist) (list (cons name val)))
        ((equal name (caar alist))
         (cons (cons name val) (cdr alist)))
        (t (cons (car alist)
                 (put-assoc-equal name val (cdr alist))))))