(hons-shrink-alist! alist ans) is an alternative to hons-shrink-alist
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
something like 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 hons-acons!.
