ACL2-pc::pp
(macro)
prettyprint the current term in internal (translated) form
Example and General Form:
pp
This is the same as p (see its documentation), except that raw syntax
(internal form) is used. So for example, one would see (if x y 'nil)
rather than (and x y). Abbreviations are however still inserted, as with
p.