Major Section: ACL2-BUILT-INS
General Forms: (delete-assoc key alist) (delete-assoc key alist :test 'eql) ; same as above (eql as equality test) (delete-assoc key alist :test 'eq) ; same, but eq is equality test (delete-assoc key alist :test 'equal) ; same, but equal is equality test
(Delete-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).
The guard for a call of delete-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
delete-assoc and its variants:
(delete-assoc-eq key alist)is equivalent to(delete-assoc key alist :test 'eq);
(delete-assoc-equal key alist)is equivalent to(delete-assoc key alist :test 'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function delete-assoc-equal.
