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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
|
<html>
<head><title>EVENTS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>EVENTS</h1>functions that extend the logic
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
<p>
<ul>
<li><h3><a href="ADD-BINOP.html">ADD-BINOP</a> -- associate a binary function name with a macro name
</h3>
</li>
<li><h3><a href="ADD-DEFAULT-HINTS.html">ADD-DEFAULT-HINTS</a> -- add to the default hints
</h3>
</li>
<li><h3><a href="ADD-DEFAULT-HINTS_bang_.html">ADD-DEFAULT-HINTS!</a> -- add to the default hints non-<code><a href="LOCAL.html">local</a></code>ly
</h3>
</li>
<li><h3><a href="ADD-DIVE-INTO-MACRO.html">ADD-DIVE-INTO-MACRO</a> -- associate <a href="PROOF-CHECKER.html">proof-checker</a> diving function with macro name
</h3>
</li>
<li><h3><a href="ADD-INCLUDE-BOOK-DIR.html">ADD-INCLUDE-BOOK-DIR</a> -- associate directory to keyword for <code><a href="INCLUDE-BOOK.html">include-book</a></code>'s <code>:dir</code> argument
</h3>
</li>
<li><h3><a href="ADD-INVISIBLE-FNS.html">ADD-INVISIBLE-FNS</a> -- make some unary functions invisible to the <a href="LOOP-STOPPER.html">loop-stopper</a> algorithm
</h3>
</li>
<li><h3><a href="ADD-MACRO-ALIAS.html">ADD-MACRO-ALIAS</a> -- associate a function name with a macro name
</h3>
</li>
<li><h3><a href="ADD-MATCH-FREE-OVERRIDE.html">ADD-MATCH-FREE-OVERRIDE</a> -- set <code>:match-free</code> value to <code>:once</code> or <code>:all</code> in existing rules
</h3>
</li>
<li><h3><a href="ADD-NTH-ALIAS.html">ADD-NTH-ALIAS</a> -- associate one symbol with another for printing of <code><a href="NTH.html">nth</a></code>/<code><a href="UPDATE-NTH.html">update-nth</a></code> terms
</h3>
</li>
<li><h3><a href="ASSERT-EVENT.html">ASSERT-EVENT</a> -- assert that a given form returns a non-<code>nil</code> value
</h3>
</li>
<li><h3><a href="BINOP-TABLE.html">BINOP-TABLE</a> -- associates binary function with the corresponding macro
</h3>
</li>
<li><h3><a href="COMP.html">COMP</a> -- compile some ACL2 functions
</h3>
</li>
<li><h3><a href="DEFABBREV.html">DEFABBREV</a> -- a convenient form of macro definition for simple expansions
</h3>
</li>
<li><h3><a href="DEFAULT-HINTS-TABLE.html">DEFAULT-HINTS-TABLE</a> -- a <a href="TABLE.html">table</a> used to provide <a href="HINTS.html">hints</a> for proofs
</h3>
</li>
<li><h3><a href="DEFAXIOM.html">DEFAXIOM</a> -- add an axiom
</h3>
</li>
<li><h3><a href="DEFCHOOSE.html">DEFCHOOSE</a> -- define a Skolem (witnessing) function
</h3>
</li>
<li><h3><a href="DEFCONG.html">DEFCONG</a> -- prove that one <a href="EQUIVALENCE.html">equivalence</a> relation preserves another in a given
<br><code> </code> argument position of a given function
</h3>
</li>
<li><h3><a href="DEFCONST.html">DEFCONST</a> -- define a constant
</h3>
</li>
<li><h3><a href="DEFDOC.html">DEFDOC</a> -- add a <a href="DOCUMENTATION.html">documentation</a> topic
</h3>
</li>
<li><h3><a href="DEFEQUIV.html">DEFEQUIV</a> -- prove that a function is an <a href="EQUIVALENCE.html">equivalence</a> relation
</h3>
</li>
<li><h3><a href="DEFEVALUATOR.html">DEFEVALUATOR</a> -- introduce an evaluator function
</h3>
</li>
<li><h3><a href="DEFEXEC.html">DEFEXEC</a> -- attach a terminating executable function to a definition
</h3>
</li>
<li><h3><a href="DEFLABEL.html">DEFLABEL</a> -- build a landmark and/or add a <a href="DOCUMENTATION.html">documentation</a> topic
</h3>
</li>
<li><h3><a href="DEFMACRO.html">DEFMACRO</a> -- define a macro
</h3>
</li>
<li><h3><a href="DEFPKG.html">DEFPKG</a> -- define a new symbol package
</h3>
</li>
<li><h3><a href="DEFREFINEMENT.html">DEFREFINEMENT</a> -- prove that <code>equiv1</code> refines <code>equiv2</code>
</h3>
</li>
<li><h3><a href="DEFSTOBJ.html">DEFSTOBJ</a> -- define a new single-threaded object
</h3>
</li>
<li><h3><a href="DEFSTUB.html">DEFSTUB</a> -- stub-out a function symbol
</h3>
</li>
<li><h3><a href="DEFTHEORY.html">DEFTHEORY</a> -- define a theory (to <a href="ENABLE.html">enable</a> or <a href="DISABLE.html">disable</a> a set of rules)
</h3>
</li>
<li><h3><a href="DEFTHM.html">DEFTHM</a> -- prove and name a theorem
</h3>
</li>
<li><h3><a href="DEFTHMD.html">DEFTHMD</a> -- prove and name a theorem and then disable it
</h3>
</li>
<li><h3><a href="DEFTTAG.html">DEFTTAG</a> -- introduce a trust tag (ttag)
</h3>
</li>
<li><h3><a href="DEFUN.html">DEFUN</a> -- define a function symbol
</h3>
</li>
<li><h3><a href="DEFUN-SK.html">DEFUN-SK</a> -- define a function whose body has an outermost quantifier
</h3>
</li>
<li><h3><a href="DEFUND.html">DEFUND</a> -- define a function symbol and then disable it
</h3>
</li>
<li><h3><a href="DELETE-INCLUDE-BOOK-DIR.html">DELETE-INCLUDE-BOOK-DIR</a> -- remove association of keyword for <code><a href="INCLUDE-BOOK.html">include-book</a></code>'s <code>:dir</code> argument
</h3>
</li>
<li><h3><a href="DIVE-INTO-MACROS-TABLE.html">DIVE-INTO-MACROS-TABLE</a> -- right-associated function information for the <a href="PROOF-CHECKER.html">proof-checker</a>
</h3>
</li>
<li><h3><a href="ENCAPSULATE.html">ENCAPSULATE</a> -- constrain some functions and/or hide some <a href="EVENTS.html">events</a>
</h3>
</li>
<li><h3><a href="IN-ARITHMETIC-THEORY.html">IN-ARITHMETIC-THEORY</a> -- designate ``current'' theory for some rewriting done in linear arithmetic
</h3>
</li>
<li><h3><a href="IN-THEORY.html">IN-THEORY</a> -- designate ``current'' theory (enabling its rules)
</h3>
</li>
<li><h3><a href="INCLUDE-BOOK.html">INCLUDE-BOOK</a> -- load the <a href="EVENTS.html">events</a> in a file
</h3>
</li>
<li><h3><a href="INVISIBLE-FNS-TABLE.html">INVISIBLE-FNS-TABLE</a> -- functions that are invisible to the <a href="LOOP-STOPPER.html">loop-stopper</a> algorithm
</h3>
</li>
<li><h3><a href="LOCAL.html">LOCAL</a> -- hiding an event in an encapsulation or book
</h3>
</li>
<li><h3><a href="LOGIC.html">LOGIC</a> -- to set the default <a href="DEFUN-MODE.html">defun-mode</a> to <code>:logic</code>
</h3>
</li>
<li><h3><a href="MACRO-ALIASES-TABLE.html">MACRO-ALIASES-TABLE</a> -- a <a href="TABLE.html">table</a> used to associate function names with macro names
</h3>
</li>
<li><h3><a href="MAKE-EVENT.html">MAKE-EVENT</a> -- evaluate (expand) a given form and then evaluate the result
</h3>
</li>
<li><h3><a href="MUTUAL-RECURSION.html">MUTUAL-RECURSION</a> -- define some mutually recursive functions
</h3>
</li>
<li><h3><a href="NTH-ALIASES-TABLE.html">NTH-ALIASES-TABLE</a> -- a <a href="TABLE.html">table</a> used to associate names for nth/update-nth printing
</h3>
</li>
<li><h3><a href="PROGN.html">PROGN</a> -- evaluate some <a href="EVENTS.html">events</a>
</h3>
</li>
<li><h3><a href="PROGN_bang_.html">PROGN!</a> -- evaluate some forms, not necessarily <a href="EVENTS.html">events</a>
</h3>
</li>
<li><h3><a href="PROGRAM.html">PROGRAM</a> -- to set the default <a href="DEFUN-MODE.html">defun-mode</a> to <code>:</code><code><a href="PROGRAM.html">program</a></code>
</h3>
</li>
<li><h3><a href="PUSH-UNTOUCHABLE.html">PUSH-UNTOUCHABLE</a> -- add name or list of names to the list of untouchable symbols
</h3>
</li>
<li><h3><a href="REDO-FLAT.html">REDO-FLAT</a> -- redo up through a failure in an <code><a href="ENCAPSULATE.html">encapsulate</a></code> or <code><a href="PROGN.html">progn</a></code>
</h3>
</li>
<li><h3><a href="REMOVE-BINOP.html">REMOVE-BINOP</a> -- remove the association of a binary function name with a macro name
</h3>
</li>
<li><h3><a href="REMOVE-DEFAULT-HINTS.html">REMOVE-DEFAULT-HINTS</a> -- remove from the default hints
</h3>
</li>
<li><h3><a href="REMOVE-DEFAULT-HINTS_bang_.html">REMOVE-DEFAULT-HINTS!</a> -- remove from the default hints non-<code><a href="LOCAL.html">local</a></code>ly
</h3>
</li>
<li><h3><a href="REMOVE-DIVE-INTO-MACRO.html">REMOVE-DIVE-INTO-MACRO</a> -- removes association of <a href="PROOF-CHECKER.html">proof-checker</a> diving function with macro name
</h3>
</li>
<li><h3><a href="REMOVE-INVISIBLE-FNS.html">REMOVE-INVISIBLE-FNS</a> -- make some unary functions no longer invisible
</h3>
</li>
<li><h3><a href="REMOVE-MACRO-ALIAS.html">REMOVE-MACRO-ALIAS</a> -- remove the association of a function name with a macro name
</h3>
</li>
<li><h3><a href="REMOVE-NTH-ALIAS.html">REMOVE-NTH-ALIAS</a> -- remove the association of one symbol with another for printing of <code><a href="NTH.html">nth</a></code>/<code><a href="UPDATE-NTH.html">update-nth</a></code> terms
</h3>
</li>
<li><h3><a href="REMOVE-UNTOUCHABLE.html">REMOVE-UNTOUCHABLE</a> -- remove name or list of names to the list of untouchable symbols
</h3>
</li>
<li><h3><a href="RESET-PREHISTORY.html">RESET-PREHISTORY</a> -- reset the prehistory
</h3>
</li>
<li><h3><a href="SET-BACKCHAIN-LIMIT.html">SET-BACKCHAIN-LIMIT</a> -- Sets the backchain-limit used by the rewriter
</h3>
</li>
<li><h3><a href="SET-BODY.html">SET-BODY</a> -- set the definition body
</h3>
</li>
<li><h3><a href="SET-BOGUS-MUTUAL-RECURSION-OK.html">SET-BOGUS-MUTUAL-RECURSION-OK</a> -- allow unnecessary ``mutual recursion''
</h3>
</li>
<li><h3><a href="SET-CASE-SPLIT-LIMITATIONS.html">SET-CASE-SPLIT-LIMITATIONS</a> -- set the case-split-limitations
</h3>
</li>
<li><h3><a href="SET-COMPILE-FNS.html">SET-COMPILE-FNS</a> -- have each function compiled as you go along.
</h3>
</li>
<li><h3><a href="SET-DEFAULT-BACKCHAIN-LIMIT.html">SET-DEFAULT-BACKCHAIN-LIMIT</a> -- sets the default backchain-limit used when admitting a rule
</h3>
</li>
<li><h3><a href="SET-DEFAULT-HINTS.html">SET-DEFAULT-HINTS</a> -- set the default hints
</h3>
</li>
<li><h3><a href="SET-DEFAULT-HINTS_bang_.html">SET-DEFAULT-HINTS!</a> -- set the default hints non-<code><a href="LOCAL.html">local</a></code>ly
</h3>
</li>
<li><h3><a href="SET-ENFORCE-REDUNDANCY.html">SET-ENFORCE-REDUNDANCY</a> -- require most events to be redundant
</h3>
</li>
<li><h3><a href="SET-IGNORE-OK.html">SET-IGNORE-OK</a> -- allow unused formals and locals without an <code>ignore</code> or <code>ignorable</code> declaration
</h3>
</li>
<li><h3><a href="SET-INHIBIT-WARNINGS.html">SET-INHIBIT-WARNINGS</a> -- control warnings
</h3>
</li>
<li><h3><a href="SET-INVISIBLE-FNS-TABLE.html">SET-INVISIBLE-FNS-TABLE</a> -- set the invisible functions table
</h3>
</li>
<li><h3><a href="SET-IRRELEVANT-FORMALS-OK.html">SET-IRRELEVANT-FORMALS-OK</a> -- allow irrelevant formals in definitions
</h3>
</li>
<li><h3><a href="SET-LET_star_-ABSTRACTIONP.html">SET-LET*-ABSTRACTIONP</a> -- to shorten many prettyprinted clauses
</h3>
</li>
<li><h3><a href="SET-MATCH-FREE-DEFAULT.html">SET-MATCH-FREE-DEFAULT</a> -- provide default for <code>:match-free</code> in future rules
</h3>
</li>
<li><h3><a href="SET-MATCH-FREE-ERROR.html">SET-MATCH-FREE-ERROR</a> -- control error vs. warning when <code>:match-free</code> is missing
</h3>
</li>
<li><h3><a href="SET-MEASURE-FUNCTION.html">SET-MEASURE-FUNCTION</a> -- set the default measure function symbol
</h3>
</li>
<li><h3><a href="SET-NON-LINEARP.html">SET-NON-LINEARP</a> -- to turn on or off non-linear arithmetic reasoning
</h3>
</li>
<li><h3><a href="SET-NU-REWRITER-MODE.html">SET-NU-REWRITER-MODE</a> -- to turn on and off the nu-rewriter
</h3>
</li>
<li><h3><a href="SET-REWRITE-STACK-LIMIT.html">SET-REWRITE-STACK-LIMIT</a> -- Sets the rewrite stack depth used by the rewriter
</h3>
</li>
<li><h3><a href="SET-STATE-OK.html">SET-STATE-OK</a> -- allow the use of STATE as a formal parameter
</h3>
</li>
<li><h3><a href="SET-VERIFY-GUARDS-EAGERNESS.html">SET-VERIFY-GUARDS-EAGERNESS</a> -- the eagerness with which <a href="GUARD.html">guard</a> verification is tried.
</h3>
</li>
<li><h3><a href="SET-WELL-FOUNDED-RELATION.html">SET-WELL-FOUNDED-RELATION</a> -- set the default well-founded relation
</h3>
</li>
<li><h3><a href="TABLE.html">TABLE</a> -- user-managed tables
</h3>
</li>
<li><h3><a href="TERM-TABLE.html">TERM-TABLE</a> -- a table used to validate meta rules
</h3>
</li>
<li><h3><a href="THEORY-INVARIANT.html">THEORY-INVARIANT</a> -- user-specified invariants on <a href="THEORIES.html">theories</a>
</h3>
</li>
<li><h3><a href="USER-DEFINED-FUNCTIONS-TABLE.html">USER-DEFINED-FUNCTIONS-TABLE</a> -- an advanced <a href="TABLE.html">table</a> used to replace certain system functions
</h3>
</li>
<li><h3><a href="VERIFY-GUARDS.html">VERIFY-GUARDS</a> -- verify the <a href="GUARD.html">guard</a>s of a function
</h3>
</li>
<li><h3><a href="VERIFY-TERMINATION.html">VERIFY-TERMINATION</a> -- convert a function from :program mode to :logic mode
</h3>
</li>
<li><h3><a href="WITH-OUTPUT.html">WITH-OUTPUT</a> -- suppressing or turning on specified output for an event
</h3>
</li>
</ul>
Any extension of the syntax of ACL2 (i.e., the definition of a new
constant or macro), the axioms (i.e., the definition of a function),
or the rule data base (i.e., the proof of a theorem), constitutes a
logical ``event.'' Events change the ACL2 logical world
(see <a href="WORLD.html">world</a>). Indeed, the only way to change the ACL2
<a href="WORLD.html">world</a> is via the successful evaluation of an event function.
Every time the <a href="WORLD.html">world</a> is changed by an event, a landmark is left
on the <a href="WORLD.html">world</a> and it is thus possible to identify the <a href="WORLD.html">world</a>
``as of'' the evaluation of a given event. An event may introduce
new logical names. Some events introduce no new names (e.g.,
<code><a href="VERIFY-GUARDS.html">verify-guards</a></code>), some introduce exactly one (e.g., <code><a href="DEFMACRO.html">defmacro</a></code> and
<code><a href="DEFTHM.html">defthm</a></code>), and some may introduce many (e.g., <code><a href="ENCAPSULATE.html">encapsulate</a></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>
|
