Major Section: ACL2-BUILT-INS
(Acons key datum alist) equals the result of consing the pair
(cons key datum) to the front of the association list alist.
(Acons key datum alist) has a guard of (alistp alist).
Acons is a Common Lisp function. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.
