ACL2-pc::p-top
(macro)
prettyprint the conclusion, highlighting the current term
Example and General Form:
p-top
For example, if the conclusion is (equal (and x (p y)) (foo z)) and
the current subterm is (p y), then p-top will print (equal (and x
(*** (p y) ***)) (foo z)).
Prettyprint the conclusion, highlighting the current term. The usual
user syntax is used, as with the command p (as opposed to pp). This
is illustrated in the example above, where one would *not* see
(equal (if x (*** (p y) ***) 'nil) (foo z)).
Remark (obscure): In some situations, a term of the form (if x t
y) occurring inside the current subterm will not print as (or x y),
when x isn't a call of a boolean primitive. There's nothing incorrect
about this, however.
