1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
<html>
<head><title>Q.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>Q</h2>quit ACL2 (type <code>:q</code>) -- reenter with <code>(lp)</code>
<pre>Major Section: <a href="OTHER.html">OTHER</a>
</pre><p>
<pre>
Example:
ACL2 !>:Q
</pre>
<p>
The keyword command <code>:q</code> 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 <code><a href="LP.html">lp</a></code>). To reenter
the ACL2 loop, execute <code>(acl2::lp)</code> in Common Lisp. You will be in
the same state as you were when you exited with <code>:q</code>, unless during
your stay in Common Lisp you messed the data structures
representating the ACL2 <a href="STATE.html">state</a> (including files, property lists,
and single-threaded objects).<p>
Unlike all other keyword commands, typing <code>:q</code> is not equivalent to
invoking the function <code>q</code>. There is no function <code>q</code>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
