quit ACL2 (type :q) -- reenter with (lp)
Major Section:  OTHER

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 the data structures representating 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.