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.