(hons-copy-persistent x) returns a normed object that is equal to X
and which will be re-normed after any calls to hons-clear.
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 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
hons-copy.
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 hons-copy.
