Cause an immediate Lisp break
ACL2 users are generally advised to avoid breaking into raw Lisp.
Advanced users may, on occasion, see the need to do so. Evaluating
(break$) will have that effect. (Exception: break$ is disabled
after evaluation of (set-debugger-enable :never); see set-debugger-enable.) Break$ returns nil. Note that upon
returning to the ACL2 read-eval-print loop (for example, using :q if the
host Lisp is CCL), one will be at the top level even if one had been inside a
recursive call of ld or a wormhole.
(defun break$ nil
(declare (xargs :guard t))