Print the translation of a form without code restrictions
:trans! (list a b c)
:trans! (append x state)
:trans! (cons (mv 3 4) x)
:Trans! is identical to :trans, except that :trans!
is more permissive: it allows expressions that may occur in theorems but are
illegal in code. In particular, :trans! allows violations of
single-threadedness and multiple-value restrictions. Thus, the second and
third forms above are legal for :trans! even though they are illegal for
:trans. Also see trans, see trans1, and see trans*.