(hons-assoc-equal key alist) is not fast; it serves as the logical
definition for hons-get.
Major Section: HONS-AND-MEMOIZATION
This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.
The definition of hons-assoc-equal is similar to that of assoc-equal,
except that (1) it does not require alistp as a guard, and (2) it "skips
over" any non-conses when its alist argument is malformed.
We typically leave hons-get enabled and reason about hons-assoc-equal
instead. One benefit of this approach is that it avoids certain "false"
discipline warnings that might arise from execution during theorem proving.
