ACL2-PC::P

(macro) prettyprint the current term
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
p

Prettyprint the current term. The usual user syntax is used, so that for example one would see (and x y) rather than (if x y 'nil). (See also pp.) Also, abbreviations are inserted where appropriate; see add-abbreviation.

The ``current term'' is the entire conclusion unless dive commands have been given, in which case it may be a subterm of the conclusion.

If all goals have been proved, a message saying so will be printed (as there will be no current term!).