(hons-assoc-equal key alist)is not fast; it serves as the logical
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
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
instead. One benefit of this approach is that it avoids certain "false"
discipline warnings that might arise from execution during theorem proving.