(hons-assoc-equal key alist) is not fast; it serves as the logical definition for hons-get.

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.