Show a user-level representation of a term

ACL2 uses a strict notion of ``term'' for its internal
computations; see pseudo-termp. Such expressions are sometimes called
``translated terms''. However, ACL2 provides user-level output —
for example, in output from the theorem prover — in the form of
so-called ``untranslated terms''. For example, the untranslated term `trans` to the untranslated term:

ACL2 !>:trans (<= 3 x) (NOT (< X '3)) => * ACL2 !>

Notice for example that the macro

The call

ACL2 !>:trans (and x t) (IF X 'T 'NIL) => * ACL2 !>(untranslate '(IF X 'T 'NIL) nil (w state)) (AND X T) ACL2 !>(untranslate '(IF X 'T 'NIL) t (w state)) X ACL2 !>

The latter result,

ACL2 !>:trans (if (and x t) y z) (IF (IF X 'T 'NIL) Y Z) => * ACL2 !>(untranslate '(IF (IF X 'T 'NIL) Y Z) nil (w state)) (IF X Y Z) ACL2 !>

Also see user-defined-functions-table and add-macro-fn.