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).
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).