P!
To pop up (at least) one level of ACL2's command loop
Logically speaking, (p!) = nil. If you are already at the top
level of the ACL2 command loop, rather than being in a subsidiary call of
ld, then the keyword then a call of (p!) returns nil and has
no other effect.
Otherwise, (p!) is evaluated inside a call of ld that was made
inside ACL2's command loop. In that case, the current computation is aborted
and treating as causing an error, and control returns to the superior call of
ld.
Here is a more detailed description of the effect of (p!) when not at
the top level of the ACL2 command loop. The current call of LD is
treated as though ld-error-action is :RETURN! (the default; here we
ignore the case (:exit N)) and hence immediately returns control to the
superior call of ld. If all calls of ld were made with the
default ld-error-action of :RETURN!, then all superior calls of
ld will then complete until you are back at top level of the ACL2 loop.
For more information, see ld-error-action.
If you are at an ACL2 prompt (as opposed to a raw Lisp break), then you may
type :p! in place of (p!); see keyword-commands.
If you are actually in a break caused by break-rewrite, :p! and
(p!) just print a message and otherwise are no-ops. (A comment in the
source code definition of p! explains why break-rewrite cannot support
``popping up one level'' in the sense that you would probably expect.)
