HONS-ASSOC-EQUAL

(hons-assoc-equal key alist) is not fast; it serves as the logical definition for hons-get.
Major Section:  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.