Hons-copy-persistent
(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.
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.
Function: hons-copy-persistent
(defun hons-copy-persistent (x)
(declare (xargs :guard t))
x)