A!
To return to the top-level of ACL2's command loop
When (a!) is evaluated inside of ACL2's command loop, the
current computation is aborted and control returns to the top of the command
loop, exactly as though the user had interrupted and aborted the current
computation. (Note: Versions of ACL2 up to Version_3.4 provided `#.' for
this purpose, but no longer; see sharp-dot-reader.)
If you are at an ACL2 prompt (as opposed to a raw Lisp break), then you may
type :a! in place of (a!); see keyword-commands.
For a related feature that only pops up one level of ld, see p!. However, p! behaves differently if you're typing to the interactive
break caused by break-rewrite. Instead of popping up one level,
p! in break-rewrite prints a message and is otherwise a no-op.
Logically speaking, (a!) = nil. But imagine that it is defined in
such a way that it causes a stack overflow or other resource exhaustion when
called.
