(a!) = nil. But imagine that it is defined in such a
way that it causes a stack overflow or other resource exhaustion when
called.
Major Section: MISCELLANEOUS
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.)
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.