(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.
prettyprint the conclusion, highlighting the current term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: p-topFor 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 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)).
Note (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.