HONS-GET

assoc-equal for hons 
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-GET is merely another name for the ASSOC-EQUAL function when the guard of ASSOC-EQUAL 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.