(hons-copy-persistent x)returns a normed object that is equal to X
and which will be re-normed after any calls to
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.
hons-copy-persistent is the identity; we leave it enabled and
would think it odd to ever prove a theorem about it.
Under the hood,
hons-copy-persistent is virtually identical to
The only difference is that when
hons-clear is used, any persistently
normed conses are automatically re-normed, and this re-norming can be carried
out more efficiently than, say, an ordinary