constructor for association lists
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.