P!

to pop up (at least) one level of ACL2's command loop
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.