(hons-shrink-alist! alist ans)is an alternative to
that produces a normed result.
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.
Logically this function is just
hons-shrink-alist; we leave it enabled and
would think it odd to ever prove a theorem about it.
Under the hood, this is the same as
hons-shrink-alist except that it uses
hons-acons! instead of
hons-acons. You generally
should not use this function unless you really know what you're doing and
understand the drawbacks discussed in