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
(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
This is illustrated in the example above, where one would
(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),
x isn't a call of a boolean primitive. There's nothing
incorrect about this, however.