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 when the guard of
is satisfied, i.e., the following is a theorem.
(implies (alistp alist) (equal (hons-get key alist) (assoc-equal key alist)))
If alist has been formed via calls to HONS-ACONS, HONS-GET should operate at hash-table lookup speed.
HONS-GET has an 'under the hood' implementation.