:q
) -- reenter with (lp)
Major Section: OTHER
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 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
.