Major Section: MISCELLANEOUS
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) 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.
