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.
hons-get is merely another name for the
assoc-equal function, i.e., the following is a theorem.
(equal (hons-get key alist) (assoc-equal key alist))
If alist has be formed via calls to HONS-ACONS, hons-get should operate at hash-table lookup speed.
Has an 'under the hood' implementation.