(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.

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.