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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
<html>
<head><title>OTHER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>OTHER</h1>other commonly used top-level functions
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
<p>
<ul>
<li><h3><a href="_at_.html">@</a> -- get the value of a global variable in <code><a href="STATE.html">state</a></code>
</h3>
</li>
<li><h3><a href="ACL2-DEFAULTS-TABLE.html">ACL2-DEFAULTS-TABLE</a> -- a <a href="TABLE.html">table</a> specifying certain defaults, e.g., the default <a href="DEFUN-MODE.html">defun-mode</a>
</h3>
</li>
<li><h3><a href="ACL2-HELP.html">ACL2-HELP</a> -- the acl2-help mailing list
</h3>
</li>
<li><h3><a href="ASSIGN.html">ASSIGN</a> -- assign to a global variable in <code><a href="STATE.html">state</a></code>
</h3>
</li>
<li><h3><a href="CERTIFY-BOOK.html">CERTIFY-BOOK</a> -- how to produce a <a href="CERTIFICATE.html">certificate</a> for a book
</h3>
</li>
<li><h3><a href="CERTIFY-BOOK_bang_.html">CERTIFY-BOOK!</a> -- a variant of <code><a href="CERTIFY-BOOK.html">certify-book</a></code>
</h3>
</li>
<li><h3><a href="CW-GSTACK.html">CW-GSTACK</a> -- debug a rewriting loop or stack overflow
</h3>
</li>
<li><h3><a href="EXIT.html">EXIT</a> -- quit entirely out of Lisp
</h3>
</li>
<li><h3><a href="GOOD-BYE.html">GOOD-BYE</a> -- quit entirely out of Lisp
</h3>
</li>
<li><h3><a href="IN-PACKAGE.html">IN-PACKAGE</a> -- select current package
</h3>
</li>
<li><h3><a href="LD.html">LD</a> -- the ACL2 read-eval-print loop, file loader, and <a href="COMMAND.html">command</a> processor
</h3>
</li>
<li><h3><a href="PROPS.html">PROPS</a> -- print the ACL2 properties on a symbol
</h3>
</li>
<li><h3><a href="PSO.html">PSO</a> -- show the most recently saved output
</h3>
</li>
<li><h3><a href="PSO_bang_.html">PSO!</a> -- show the most recently saved output, including <a href="PROOF-TREE.html">proof-tree</a> output
</h3>
</li>
<li><h3><a href="PSTACK.html">PSTACK</a> -- seeing what is the prover up to
</h3>
</li>
<li><h3><a href="Q.html">Q</a> -- quit ACL2 (type <code>:q</code>) -- reenter with <code>(lp)</code>
</h3>
</li>
<li><h3><a href="QUIT.html">QUIT</a> -- quit entirely out of Lisp
</h3>
</li>
<li><h3><a href="REBUILD.html">REBUILD</a> -- a convenient way to reconstruct your old <a href="STATE.html">state</a>
</h3>
</li>
<li><h3><a href="RESET-LD-SPECIALS.html">RESET-LD-SPECIALS</a> -- restores initial settings of the <code><a href="LD.html">ld</a></code> specials
</h3>
</li>
<li><h3><a href="SAVE-EXEC.html">SAVE-EXEC</a> -- save an executable image and (for most Common Lisps) a wrapper script
</h3>
</li>
<li><h3><a href="SET-GUARD-CHECKING.html">SET-GUARD-CHECKING</a> -- control checking <a href="GUARD.html">guard</a>s during execution of top-level forms
</h3>
</li>
<li><h3><a href="SET-INHIBIT-OUTPUT-LST.html">SET-INHIBIT-OUTPUT-LST</a> -- control output
</h3>
</li>
<li><h3><a href="SET-LD-REDEFINITION-ACTION.html">SET-LD-REDEFINITION-ACTION</a> -- See <a href="LD-REDEFINITION-ACTION.html">ld-redefinition-action</a>.
</h3>
</li>
<li><h3><a href="SET-LD-SKIP-PROOFSP.html">SET-LD-SKIP-PROOFSP</a> -- See <a href="LD-SKIP-PROOFSP.html">ld-skip-proofsp</a>.
</h3>
</li>
<li><h3><a href="SET-PRINT-CLAUSE-IDS.html">SET-PRINT-CLAUSE-IDS</a> -- cause subgoal numbers to be printed when <code>'prove</code> output is inhibited
</h3>
</li>
<li><h3><a href="SET-RAW-MODE.html">SET-RAW-MODE</a> -- enter or exit ``raw mode,'' a raw Lisp environment
</h3>
</li>
<li><h3><a href="SET-RAW-MODE-ON_bang_.html">SET-RAW-MODE-ON!</a> -- enter ``raw mode,'' a raw Lisp environment
</h3>
</li>
<li><h3><a href="SET-SAVED-OUTPUT.html">SET-SAVED-OUTPUT</a> -- save proof output for later display with <code>:</code><code><a href="PSO.html">pso</a></code> or <code>:</code><code><a href="PSO_bang_.html">pso!</a></code>
</h3>
</li>
<li><h3><a href="SET-TAINTED-OKP.html">SET-TAINTED-OKP</a> -- control output
</h3>
</li>
<li><h3><a href="SKIP-PROOFS.html">SKIP-PROOFS</a> -- skip proofs for a given form -- a quick way to introduce unsoundness
</h3>
</li>
<li><h3><a href="THM.html">THM</a> -- prove a theorem
</h3>
</li>
<li><h3><a href="TIME$.html">TIME$</a> -- time a form
</h3>
</li>
<li><h3><a href="TRANS.html">TRANS</a> -- print the macroexpansion of a form
</h3>
</li>
<li><h3><a href="TRANS_bang_.html">TRANS!</a> -- print the macroexpansion of a form without single-threadedness concerns
</h3>
</li>
<li><h3><a href="TRANS1.html">TRANS1</a> -- print the one-step macroexpansion of a form
</h3>
</li>
<li><h3><a href="WITH-PROVER-TIME-LIMIT.html">WITH-PROVER-TIME-LIMIT</a> -- limit the time for proofs
</h3>
</li>
</ul>
This section contains an assortment of top-level functions that fit into none
of the other categories and yet are suffiently useful as to merit
``<code>advertisement</code>'' in the <code>:</code><code><a href="HELP.html">help</a></code> command.
<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>
|
