ESCAPE-TO-COMMON-LISP

escaping to Common Lisp
Major Section:  MISCELLANEOUS

Example:
ACL2 !>:Q

There is no Common Lisp escape feature in the lp. This is part of the price of purity. To execute a form in Common Lisp as opposed to ACL2, exit lp with :q, submit the desired forms to the Common Lisp read-eval-print loop, and reenter ACL2 with (lp).