In the logic,
Under the hood,
What might this involve?
If X is a symbol, character, or number, then it is already normed and nothing is done.
If X is a string, we check if any normed version of X already exists. If so, we return the already-normed version; otherwise, we install X as the normed version for all strings that are equal to X.
If X is a cons, we must determine if there is a normed version of X, or recursively construct and install one. Norming large cons trees can become expensive, but there are a couple of cheap cases. In particular, if X is already normed, or if large subtrees of X are already normed, then not much needs to be done. The slowest case is norming some large ACL2 cons structure that has no subtrees which are already normed.
Note that running
(defun hons-copy (x) (declare (xargs :guard t)) x)