LOCAL

hiding an event in an encapsulation or book 
Major Section:  EVENTS


Examples:
(local (defthm hack1
         (implies (and (acl2-numberp x)
                       (acl2-numberp y)
                       (equal (* x y) 1))
                  (equal y (/ x)))))


(local (defun double-naturals-induction (a b)
         (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b))
                (double-naturals-induction (1- a) (1- b)))
               (t (list a b)))))


General Form:
(local ev)
where ev is an event form. If the current default defun-mode (see default-defun-mode) is :logic and ld-skip-proofsp is nil or t, then (local ev) is equivalent to ev. But if the current default defun-mode is :program or if ld-skip-proofsp is 'include-book, then (local ev) is a no-op. Thus, if such forms are in the event list of an encapsulate event or in a book, they are processed when the encapsulation or book is checked for admissibility in :logic mode but are skipped when extending the host world. Such events are thus considered ``local'' to the verification of the encapsulation or book. The non-local events are the ones ``exported'' by the encapsulation or book. See encapsulate for a thorough discussion. Also see local-incompatibility for a discussion of a commonly encountered problem with such event hiding: you can't make an event local if its presence is required to make sense of a non-local one.

Note that events that change the default defun-mode, and in fact any events that set the acl2-defaults-table, are disallowed inside the scope of local. See embedded-event-form.












































































LOGIC

to set the default defun-mode to :logic 
Major Section:  EVENTS


Example:
ACL2 p!>:logic
ACL2 !>
Typing the keyword :logic sets the default defun-mode to :logic.

Functions defined in :logic mode are logically defined. See defun-mode.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

See defun-mode for a discussion of the defun-modes available and what their effects on the logic are. See default-defun-mode for a discussion of how the default defun-mode is used. This event is equivalent to (table acl2-defaults-table :defun-mode :logic). See acl2-defaults-table.

Recall that the top-level form :logic is equivalent to (logic); see keyword-commands. Thus, to change the default defun-mode to :logic in a book, use (logic), which is an embedded event form, rather than :logic, which is not a legal form for books. See embedded-event-form.












































































MACRO-ALIASES-TABLE

a table used to associate function names with macro names 
Major Section:  EVENTS


Example:
(table macro-aliases-table 'append 'binary-append)
This example associates the function symbol binary-append with the macro name append. As a result, the name append may be used as a runic designator (see theories) by the various theory functions. Thus, for example, it will be legal to write 
(in-theory (disable append))
as an abbreviation for 
(in-theory (disable binary-append))
which in turn really abbreviates 
(in-theory (set-difference-theories (current-theory :here)
                                    '(binary-append)))


General Form:
 
(table macro-aliases-table 'macro-name 'function-name)
or very generally 
(table macro-aliases-table macro-name-form function-name-form)
where macro-name-form and function-name-form evaluate, respectively, to a macro name and a function name in the current ACL2 world. See table for a general discussion of tables and the table event used to manipulate tables.

The table macro-aliases-table is an alist that associates macro symbols with function symbols, so that macro names may be used as runic designators (see theories). For a convenient way to add entries to this table, see add-macro-alias. To remove entries from the table with ease, see remove-macro-alias.

This table is used by the theory functions. For example, in order that (disable append) be interpreted as (disable binary-append), it is necessary that the example form above has been executed. In fact, this table does indeed associate many of the macros provided by the ACL2 system, including append, with function symbols. Loosely speaking, it only does so when the macro is ``essentially the same thing as'' a corresponding function; for example, (append x y) and (binary-append x y) represent the same term, for any expressions x and y.












































































MUTUAL-RECURSION

define some mutually recursive functions 
Major Section:  EVENTS


Example:
(mutual-recursion
 (defun evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (defun oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))


General Form:
(mutual-recursion def1 ... defn)
where each defi is a DEFUN form.
When mutually recursive functions are introduced it is necessary to do the termination analysis on the entire clique of definitions. Each defun form specifies its own measure, either with the :measure keyword xarg (see xargs) or by default to acl2-count. When a function in the clique calls a function in the clique, the measure of the callee's actuals must be smaller than the measure of the caller's formals -- just as in the case of a simply recursive function. But with mutual recursion, the callee's actuals are measured as specified by the callee's defun while the caller's formals are measured as specified by the caller's defun. These two measures may be different but must be comparable in the sense that e0-ord-< decreases through calls.

The guard analysis must also be done for all of the functions at the same time. If any one of the defuns specifies the :verify-guards xarg to be nil, then guard verification is omitted for all of the functions.

Technical Note: Each defi above must be of the form (defun ...). In particular, it is not permitted for a defi to be a form that will macroexpand into a defun form. This is because mutual-recursion is itself a macro, and since macroexpansion occurs from the outside in, at the time (mutual-recursion def1 ... defk) is expanded the defi have not yet been. But mutual-recursion must decompose the defi. We therefore insist that they be explicitly presented as defuns.

Suppose you have defined your own defun-like macro and wish to use it in a mutual-recursion expression. Well, you can't. (!) But you can define your own version of mutual-recursion that allows your defun-like form. Here is an example. Suppose you define 

(defmacro my-defun (&rest args) (my-defun-fn args))
where my-defun-fn takes the arguments of the my-defun form and produces from them a defun form. As noted above, you are not allowed to write (mutual-recursion (my-defun ...) ...). But you can define the macro my-mutual-recursion so that 
(my-mutual-recursion (my-defun ...) ... (my-defun ...))
expands into (mutual-recursion (defun ...) ... (defun ...)) by applying my-defun-fn to each of the arguments of my-mutual-recursion. 
(defun my-mutual-recursion-fn (lst) 
  (declare (xargs :guard (alistp lst)))


; Each element of lst must be a consp (whose car, we assume, is always
; MY-DEFUN).  We apply my-defun-fn to the arguments of each element and
; collect the resulting list of DEFUNs.


  (cond ((atom lst) nil)
        (t (cons (my-defun-fn (cdr (car lst)))
                 (my-mutual-recursion-fn (cdr lst))))))


(defmacro my-mutual-recursion (&rest lst)


; Each element of lst must be a consp (whose car, we assume, is always
; MY-DEFUN).  We obtain the DEFUN corresponding to each and list them
; all inside a MUTUAL-RECURSION form.


  (declare (xargs :guard (alistp lst)))
  (cons 'mutual-recursion (my-mutual-recursion-fn lst))).













































































PROGRAM

to set the default defun-mode to :program 
Major Section:  EVENTS


Example:
ACL2 !>:program
ACL2 p!>
Typing the keyword :program sets the default defun-mode to :program.

Functions defined in :program mode are logically undefined but can be executed on constants outside of deductive contexts. See defun-mode.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

See defun-mode for a discussion of the defun-modes available and what their effects on the logic are. See default-defun-mode for a discussion of how the default defun-mode is used. This event is equivalent to (table acl2-defaults-table :defun-mode :program). See acl2-defaults-table.

Recall that the top-level form :program is equivalent to (program); see keyword-commands. Thus, to change the default defun-mode to :program in a book, use (program), which is an embedded event form, rather than :program, which is not a legal form for books. See embedded-event-form.












































































PUSH-UNTOUCHABLE

add name or list of names to the list of untouchable symbols 
Major Section:  EVENTS


Example:
(push-untouchable set-mem)


General Form:
(push-untouchable name :doc doc-string) or
(push-untouchable names :doc doc-string)

where name is a non-nil symbol or a true list of symbols and doc-string is an optional documentation string not beginning with ``:doc-section ...''. If name is a symbol it is treated as the singleton list containing that symbol. The effect of this event is to union the given symbols into the ``untouchables'' list in the current world. This event is redundant if every symbol listed is already a member of untouchables.

When a symbol is on the untouchables list it is syntactically illegal for any event to call a function of that name or to change the value of a state global variable of that name. Thus, the effect of pushing a function symbol, name, onto untouchables is to prevent any future event from using that symbol. This is generally done to ``fence off'' some primitive function symbol from ``users'' after the developer has used the symbol freely in the development of some higher level mechanism.












































































REMOVE-MACRO-ALIAS

remove the association of a function name with a macro name 
Major Section:  EVENTS


Example:
(remove-macro-alias append)


General Form:
(remove-macro-alias macro-name)
See macro-aliases-table for a discussion of macro aliases; also see add-macro-alias. This form sets macro-aliases-table to the result of deleting the key macro-name from that table. If the name does not occur in the table, then this form still generates an event, but the event has no real effect.












































































SET-BOGUS-MUTUAL-RECURSION-OK

allow unnecessary ``mutual recursion'' 
Major Section:  EVENTS


Examples:
(set-bogus-mutual-recursion-ok t)
(set-bogus-mutual-recursion-ok nil)
(set-bogus-mutual-recursion-ok :warn)
By default, ACL2 checks that when a ``clique'' of more than one function is defined simultaneously (using mutual-recursion or defuns), then every body calls at least one of the functions in the ``clique.'' Below, we refer to definitional events that fail this check as ``bogus'' mutual recursions. The check is important because ACL2 does not store induction schemes for functions defined with other functions in a mutual-recursion or defuns event. Thus, ACL2 may have difficulty proving theorems by induction that involve such functions. Moreover, the check can call attention to bugs, since users generally intend that their mutual recursions are not bogus.

Nevertheless, there are times when it is advantageous to allow bogus mutual recursions, for example when they are generated mechanically, even at the expense of losing stored induction schemes. The first example above allows bogus mutual recursion. The second example disallows bogus mutual recursion; this is the default. The third example allows bogus mutual recursion, but prints an appropriate warning.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-bogus-mutual-recursion-ok flg)
where flg is either t, nil, or :warn.












































































SET-COMPILE-FNS

have each function compiled as you go along. 
Major Section:  EVENTS


Example Forms:
(set-compile-fns t)    ; new functions compiled after DEFUN
(set-compile-fns nil)  ; new functions not compiled after DEFUN
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

Also see comp, because it may be more efficient in some Common Lisps to compile many functions at once rather than to compile each one as you go along. 

General Form:
(set-compile-fns term)
where term is a variable-free term that evaluates to t or nil. This macro is equivalent to 
(table acl2-defaults-table :compile-fns term).
However, unlike that simple call of the table event function (see table), no output results from a set-compile-fns event.

Set-compile-fns may be thought of as an event that merely sets a flag to t or nil. The flag's effect is felt when functions are defined, as with defun. If the flag is t, functions are automatically compiled after they are defined, as are their executable counterparts (see executable-counterpart). Otherwise, functions are not automatically compiled. Because set-compile-fns is an event, the old value of the flag is restored when a set-compile-fns event is undone.

Even when :set-compile-fns t has been executed, functions are not individually compiled when processing an include-book event. If you wish to include a book of compiled functions, we suggest that you first certify it with the compilation flag set; see certify-book. More generally, compilation via set-compile-fns is suppressed when the state global variable ld-skip-proofsp has value 'include-book.












































































SET-IGNORE-OK

allow unused formals and locals without an ignore declaration 
Major Section:  EVENTS


Examples:
(set-ignore-ok t)
(set-ignore-ok nil)
(set-ignore-ok :warn)
The first example above allows unused formals and locals, i.e., variables that would normally have to be declared ignored. The second example disallows unused formals and locals; this is the default. The third example allows them, but prints an appropriate warning.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-ignore-ok flg)
where flg is either t, nil, or :warn.

One might find this event useful when one is generating function definitions by an automated procedure, when that procedure does not take care to make sure that all formals are actually used in the definitions that it generates.

Note: Defun will continue to report irrelevant formals even if :set-ignore-ok has been set to t, unless you also use set-irrelevant-formals-ok to instruct it otherwise.












































































SET-INHIBIT-WARNINGS

control warnings 
Major Section:  EVENTS


Examples:
(set-inhibit-warnings "theory" "use")
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-inhibit-warnings string1 string2 ...)
where each string is considered without regard to case. This macro is equivalent to (table acl2-defaults-table :inhibit-warnings lst), where lst is the list of strings supplied. This macro is an event (see table), but no output results from a set-inhibit-warnings event.

The effect of this event is to suppress any warning whose label is a member of this list (where again, case is ignored). For example, the warning 

  ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....
will not be printed if "use" (or "USE", etc.) is a member of the given list of strings.

Of course, if warnings are inhibited overall -- see set-inhibit-output-lst -- then the value of :inhibit-warnings is entirely irrelevant.












































































SET-INVISIBLE-FNS-ALIST

set the invisible functions alist 
Major Section:  EVENTS


Examples:
(set-invisible-fns-alist ((binary-+ unary--)
                          (binary-* unary-/)
                          (unary-- unary--)
                          (unary-/ unary-/)))
Among other things, the setting above has the effect of making unary-- ``invisible'' for the purposes of applying permutative :rewrite rules to binary-+ trees. Thus, arg and (unary-- arg) will be given the same weight and will be permuted so as to be adjacent. The form (invisible-fns-alist (w state)) returns the current value of the invisible functions alist.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-invisible-fns-alist alist)
where alist is either t or a true list of pairs, each element of which is of the form (fn ufn1 ... ufnk), where fn is a function symbol and each ufni is a unary function symbol. When alist is t, the initial default alist is used in its place. Modulo the replacement of alist by the default setting when alist is t, this macro is equivalent to 
(table acl2-defaults-table :invisible-fns-alist 'alist),
which is also an event (see table), but no output results from a set-invisible-fns-alist event.

The ``invisible functions alist'' is an alist that associates with certain function symbols, e.g., fn above, a set of unary functions, e.g., the ufni above. The ufni associated with fn in the invisible functions alist are said to be ``invisible with respect to fn.'' If fn is not the car of any pair on the invisible functions alist, then no function is invisible for it. Thus, setting the invisible functions alist to nil completely eliminates the consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper field of :rewrite rules to prevent the indefinite application of permutative rewrite rules. Roughly speaking, if rewrite rules are being used to permute arg and (ufni arg) inside of a nest of fn calls, and ufni is invisible with respect to fn, then arg and (ufni arg) are considered to have the same ``weight'' and will be permuted so as to end up as adjacent tips in the fn nest. See loop-stopper.












































































SET-IRRELEVANT-FORMALS-OK

allow irrelevant formals in definitions 
Major Section:  EVENTS


Examples:
(set-irrelevant-formals-ok t)
(set-irrelevant-formals-ok nil)
(set-irrelevant-formals-ok :warn)
The first example above allows irrelevant formals in definitions; see irrelevant-formals. The second example disallows irrelevant formals; this is the default. The third example allows irrelevant formals, but prints an appropriate warning.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-irrelevant-formals-ok flg)
where flg is either t, nil, or :warn.












































































SET-MEASURE-FUNCTION

set the default measure function symbol 
Major Section:  EVENTS


Examples:
(set-measure-function nqthm::count)
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-measure-function name)
where name is a function symbol of one argument. This macro is equivalent to (table acl2-defaults-table :measure-function 'name), which is also an event (see table), but no output results from a set-measure-function event.

This event sets the default measure function to name. Subsequently, if a recursively defined function is submitted to defun with no explicitly given :measure argument, defun ``guesses'' the measure (name var), where name is the then current default measure function and var is the first formal found to be tested along every branch and changed in every recursive call.












































































SET-STATE-OK

allow the use of STATE as a formal parameter 
Major Section:  EVENTS

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

In brief: The variable symbol STATE has an unusual status in ACL2. In order to use it, you either need to issue :set-state-ok t, as we explain below, or you need to declare it to be a stobj, as explained elsewhere (see declare-stobjs). Now we explain in more detail.

Because the variable symbol STATE denotes the ``current ACL2 state,'' ACL2 treats the symbol very restrictively when it occurs as a formal parameter of a defined function. The novice user, who is unlikely to be aware of the special status of that symbol, is likely to be confused when error messages about STATE are printed in response to the innocent choice of that symbol as a formal variable. Therefore the top-level ACL2 loop can operate in a mode in which STATE is simply disallowed as a formal parameter.

For a discussion of STATE, See state and see stobj. Roughly speaking, at the top-level, the ``current ACL2 state'' is denoted by the variable symbol STATE. Only the current state may be passed into a function expecting a state as an argument. Furthermore, the name of the formal parameter into which the current state is passed must be STATE and nothing but the current state may be passed into a formal of that name. Therefore, only certain access and change functions can use that formal -- namely with a STATE formal -- and if any such function produces a new state it becomes the ``current state'' and must be passed along in the STATE position thereafter. Thus, ACL2 requires that the state be single-threaded. This, in turn, allows us to represent only one state at a time and to produce new states from it destructively in a von Neumaneque fashion. The syntactic restrictions on the variable STATE are enforced by the translate mechanism (see trans and see term) when terms are read.

To prevent the novice user from seeing messages prohibiting certain uses of the variable symbol STATE ACL2 has a mode in which it simply disallows the use of that symbol as a formal parameter. Use of the symbol causes a simple error message. The system is initially in that mode.

To get out of that mode, execute: 

:set-state-ok t
It is not recommended that you do this until you have read the documentation of STATE.

To enter the mode in which use of state is prohibited as a formal parameter, do: 

:set-state-ok nil

The mode is stored in the defaults table, See acl2-defaults-table. Thus, the mode may be set locally in books.












































































SET-VERIFY-GUARDS-EAGERNESS

the eagerness with which guard verification is tried. 
Major Section:  EVENTS


Example Forms:                        try guard verification?
(set-verify-guards-eagerness 0) ; no, unless :verify-guards t
(set-verify-guards-eagerness 1) ; yes if a :guard is supplied
(set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-verify-guards-eagerness n)
where n is a variable-free term that evaluates to 0, 1, or 2. This macro is equivalent to 
(table acl2-defaults-table :verify-guards-eagerness term).
However, unlike that simple call of the table event function (see table), no output results from a set-verify-guards-eagerness event.

Set-verify-guards-eagerness may be thought of as an event that merely sets a flag to 0, 1, or 2. The flag is used by certain defun events to determine whether guard verification is tried. The flag is irrelevant to those defun events in :program mode and to those defun events in which an explicit :verify-guards setting is provided among the xargs. In the former case, guard verification is not done because it can only be done when logical functions are being defined. In the latter case, the explicit :verify-guards setting determines whether guard verification is tried. So consider a :logic mode defun in which no :verify-guards setting is provided. Is guard verification tried? The answer depends on the eagerness setting as follows. If the eagerness is 0, guard verification is not tried. If the eagerness is 1, it is tried iff a :guard is explicitly provided in the defun. If the eagerness is 2, guard verification is tried.

The default behavior of the system is as though the :verify-guards-eagerness is 1.












































































SET-WELL-FOUNDED-RELATION

set the default well-founded relation 
Major Section:  EVENTS


Examples:
(set-well-founded-relation lex2)
provided lex2 has been proved to be a well-founded relation (see well-founded-relation). Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. 

General Form:
(set-well-founded-relation rel)
where rel has been proved to be a well-founded relation on objects satisfying some predicate, mp, as described in the documentation for well-founded-relation. This macro is equivalent to (table acl2-defaults-table :well-founded-relation 'rel).

This event sets the default well-founded relation to be that imposed on mp-measures by the relation rel. Subsequently, if a recursively defined function is submitted to defun with no explicitly given :well-founded-relation argument, defun uses the default relation, rel, and the associated domain predicate mp used in its well-foundedness theorem. That is, the termination conditions generated will require proving that the measure used by the defun is an mp-measure and that in every recursive call the measure of the arguments decreases according to rel.












































































TABLE

user-managed tables 
Major Section:  EVENTS


Examples:
(table tests 1 '(...))               ; set contents of tests[1] to '(...)
(table tests 25)                     ; get contents of tests[25]
(table tests)                        ; return table tests as an alist
(table tests nil nil :clear)         ; clear table tests
(table tests nil (foo 7) :clear)     ; set table tests to (foo 7)
(table tests nil nil :guard)         ; fetch the table guard
(table tests nil nil :guard term)    ; set the table guard


General Form:
(table table-name key-term value-term op term)
where table-name is a symbol that is the name of a (possibly new) table, key-term and value-term, if present, are arbitrary terms involving (at most) the single variable world, op, if present, is one of the table operations below, and term, if present, is a term. Table returns an acl2 ``error triple.'' The effect of table on state depends on op and how many arguments are presented. Some invocations actually have no effect on the ACL2 world and hence an invocation of table is not always an ``event''. We explain below, after giving some background information.

The ACL2 system provides ``tables'' by which the user can associate one object with another. Tables are in essence just conventional association lists -- lists of pairs -- but the ACL2 environment provides a means of storing these lists in the ``ACL2 world'' of the current state. The ACL2 user could accomplish the same ends by using ACL2 ``global variables;'' however, limitations on global variable names are imposed to insure ACL2's soundness. By convention, no table is important to ACL2's soundness, even though some features of the system use tables, and the user is invited to make free use of tables. Because tables are stored in the ACL2 world they are restored by include-book and undone by :ubt. many users of Nqthm requested a facility by which user data could be saved in Nqthm ``lib files'' and tables are ACL2's answer to that request.

Abstractly, each table is an association list mapping ``keys'' to ``values.'' In addition, each table has a ``:guard,'' which is a term that must be true of any key and value used. By setting the :guard on a table you may enforce an invariant on the objects in the table, e.g., that all keys are positive integers and all values are symbols. Each table has a ``name,'' which must be a symbol. Given a table name, there are six operations one might perform on the table.

:put -- associate a value with a key (possibly changing the value currently associated with that key).

:get -- retrieve the value associated with a key (or nil if no value has been associated with that key).

:alist -- return an alist showing all keys and non-nil values in the table.

:clear -- clear the table (so that every value is nil), or if val is supplied then set table to that value (which must be an alist).

:guard -- fetch or set the :guard of the table.

When the operations above suggest that the table or its :guard are modified, what is actually meant is that the current state is redefined so that in it, the affected table name has the appropriate properties. in such cases, the table form is an event.

Table forms are commonly typed by the user while interacting with the system. :Put and :get forms are especially common. Therefore, we have adopted a positional syntax that is intended to be convenient for most applications. Essentially, some operations admit a ``short form'' of invocation. 

(table name key-term value-term :put)   ; long form
(table name key-term value-term)        ; short form
evaluates the key- and value-terms, obtaining two objects that we call key and value, checks that the key and value satisfy the :guard on the named table and then ``modifies'' the named table so that the value associated with key is value. When used like this, table is actually an event in the sense that it changes the ACL2 world. In general, the forms evaluated to obtain the key and value may involve the variable world, which is bound to the then-current world during the evaluation of the forms. However, in the special case that the table in question is named acl2-defaults-table, the key and value terms may not contain any variables. Essentially, the keys and values used in events setting the acl2-defaults-table must be explicitly given constants. See acl2-defaults-table. 
(table name key-term nil :get)          ; long form
(table name key-term)                   ; short form
evaluates the key-term (see note below), obtaining an object, key, and returns the value associated with key in the named table (or, nil if there is no value associated with key). When used like this, table is not an event; the value is simply returned. 
(table name nil nil :alist)             ; long form
(table name)                            ; short form
returns an alist representing the named table; for every key in the table with a non-nil associated value, the alist pairs the key and its value. The order in which the keys are presented is unspecified. When used like this, table is not an event; the alist is simply returned. 
(table name nil val :clear)
sets the named table to the alist val, making the checks that :put makes for each key and value of val. When used like this, table is an event because it changes the ACL2 world. 
(table name nil nil :guard)
returns the translated form of the guard of the named table. 
(table name nil nil :guard term)
Provided the named table is empty and has not yet been assigned a :guard and term (which is not evaluated) is a term that mentions at most the variables key, val and world, this event sets the :guard of the named table to term. Whenever a subsequent :put occurs, term will be evaluated with key bound to the key argument of the :put, val bound to the val argument of the :put, and world bound to the then current world. An error will be caused by the :put if the result of the evaluation is nil.

Note that it is not allowed to change the :guard on a table once it has been explicitly set. Before the :guard is explicitly set, it is effectively just t. After it is set it can be changed only by undoing the event that set it. The purpose of this restriction is to prevent the user from changing the :guards on tables provided by other people or the system.

The intuition behind the :guard mechanism on tables is to enforce invariants on the keys and values in a table, so that the values, say, can be used without run-time checking. But if the :guard of a table is sensitive to the ACL2 world, it may be possible to cause some value in the table to cease satisfying the :guard without doing any operations on the table. Consider for example the :guard ``no value in this table is the name of an event.'' As described, that is enforced each time a value is stored. Thus, 'bang can be :put in the table provided there is no event named bang. But once it is in the table, there is nothing to prevent the user from defining bang as a function, causing the table to contain a value that could not be :put there anymore. Observe that not all state-sensitive :guards suffer this problem. The :guard ``every value is an event name'' remains invariant, courtesy of the fact that undoing back through an event name in the table would necessarily undo the :put of the name into the table.

Table was designed primarily for convenient top-level use. Tables are not especially efficient. Each table is represented by an alist stored on the property list of the table name. :Get is just a getprop and assoc-equal. :Put does a getprop to the get the table alist, a put-assoc-equal to record the new association, and a putprop to store the new table alist -- plus the overhead associated with :guards and undoable events. Note that there are never duplicate keys in the resulting alist; in particular, when the operation :clear is used to install new alist, duplicate keys are removed from that alist.

A table name may be any symbol whatsoever. Symbols already in use as function or theorem names, for example, may be used as table names. Symbols in use only as table names may be defined with defun, etc. Because there are no restrictions on the user's choice of table names, table names are not included among the logical names. Thus, :pe name will never display a table event (for a logical name other than :here). Either :pe name will display a ``normal'' event such as (defun name ...) or (defthm name ...) or else :pe name will cause an error indicating that name is not a logical name. This happens even if name is in use as a table name. Similarly, we do not permit table names to have documentation strings, since the same name might already have a documentation string. If you want to associate a documentation string with a table name that is being used no other way, define the name as a label and use the :doc feature of deflabel (see deflabel); also see defdoc.