		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::p

(macro) prettyprint the current term in the usual user-level (untranslated) syntax

Example and General Form:
p

Prettyprint the current term. The usual user (untranslated) 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 ACL2-pc::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!).