Q
Quit ACL2 (type :q) — reenter with (lp)
Example:
ACL2 !>:Q
The keyword command :q typed at the top-level of the ACL2 loop will
terminate the loop and return control to the Common Lisp top-level (or, more
precisely, to whatever program invoked lp). To reenter the ACL2 loop,
execute (acl2::lp) in Common Lisp. You will be in the same state as you
were when you exited with :q, unless during your stay in Common Lisp you
messed with the data structures representing the ACL2 state (including
files, property lists, and single-threaded objects).
Unlike all other keyword commands, typing :q is not equivalent to
invoking the function q. There is no function q.
