acons with hons

This documentation topic relates to an experimental extension of ACL2 under development by Bob Boyer and Warren Hunt. See hons-and-memoization.

Logically, hons-acons is merely another name for the acons function, i.e., the following is a theorem.

(equal (hons-acons key value alist) 
       (cons (cons key value) alist))

Practically speaking, HONS-COPY is called on the KEY so that fast access with HONS-GET is a possibility.

Each time that HONS-ACONS is called when alist has an underlying hash table for fast access, that hash table is 'stolen' and associated with the result of the HONS-ACONS.

Has an 'under the hood' implementation.