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