Major Section: HONS-AND-MEMOIZATION
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.