DEFUN-SK

define a function whose body has an outermost quantifier
Major Section:  EVENTS

Examples:
(defun-sk forall-x-p-and-q (y z)
  (forall x
          (and (p x y z)
               (q x y z))))

(defun-sk forall-x-p-and-q (y z) ; equivalent to the above (forall (x) (and (p x y z) (q x y z))))

(defun-sk some-x-y-p-and-q (z) (exists (x y) (and (p x y z) (q x y z))))

General Form:
(defun-sk fn (var1 ... varn) body
  &key doc quant-ok skolem-name thm-name)
where fn is the symbol you wish to define and is a new symbolic name (see name), (var1 ... varn) is its list of formal parameters (see name), and body is its body, which must be quantified as described below. The &key argument doc is an optional documentation string to be associated with fn; for a description of its form, see doc-string. The other arguments are explained below. For a more elaborate example than those above, see Tutorial4-Defun-Sk-Example.

The third argument, body, must be of the form

(Q bound-vars term)
where: Q is the symbol forall or exists (in the "ACL2" package), bound-vars is a variable or true list of variables disjoint from (var1 ... varn) and not including state, and term is a term. The case that bound-vars is a single variable v is treated exactly the same as the case that bound-vars is (v).

The result of this event is to introduce a ``Skolem function,'' whose name is the keyword argument skolem-name if that is supplied, and otherwise is the result of modifying fn by suffixing "-WITNESS" to its name. The following definition and and of the following two theorems are introduced for skolem-name and fn in the case that bound-vars (see above) is a single variable v. The name of the defthm event may be supplied as the value of the keyword argument :thm-name; if it is not supplied, then it is the result of modifying fn by suffixing "-SUFF" to its name in the case that the quantifier is exists, and "-NECC" in the case that the quantifier is forall.

(defun fn (var1 ... varn)
  (let ((v (skolem-name var1 ... varn)))
    body))

(defthm fn-suff ;in case the quantifier is EXISTS (implies body (fn var1 ... varn)))

(defthm fn-necc ;in case the quantifier is FORALL (implies (not body) (not (fn var1 ... varn))))

In the case that bound-vars is a list of at least two variables, say (bv1 ... bvk), the definition above is the following instead, but the theorem remains unchanged.
(defun fn (var1 ... varn)
  (mv-let (bv1 ... bvk)
          (skolem-name var1 ... varn)
          body))

In order to emphasize that the last element of the list body is a term, defun-sk checks that the symbols forall and exists do not appear anywhere in it. However, on rare occasions one might deliberately choose to violate this convention, presumably because forall or exists is being used as a variable or because a macro call will be eliminating ``calls of'' forall and exists. In these cases, the keyword argument quant-ok may be supplied a non-nil value. Then defun-sk will permit forall and exists in the body, but it will still cause an error if there is a real attempt to use these symbols as quantifiers.

Those who want a more flexible version of defun-sk that allows nested quantifiers, should contact the implementors. In the meantime, if you want to represent nested quantifiers, you have to manage that yourself. For example, in order to represent

(forall x (exists y (p x y z)))
you would use defun-sk twice, for example as follows.
(defun-sk exists-y-p (x z)
  (exists y (p x y z)))

(defun-sk forall-x-exists-y-p (z) (forall x (exists-y-p x z)))

Some distracting and unimportant warnings are inhibited during defun-sk.

Defun-sk is implemented using defchoose, and hence should only be executed in defun-mode :logic; see defun-mode and see defchoose.

Note that this way of implementing quantifiers is not a new idea. Hilbert was certainly aware of it 60 years ago! The ``story'' (see bibliography) explains why our use of defchoose is appropriate, even in the presence of epsilon-0 induction.













































































EXISTS

existential quantifier
Major Section:  DEFUN-SK

The symbol exists (in the ACL2 package) represents existential quantification in the context of a defun-sk form. See defun-sk and see forall.













































































FORALL

universal quantifier
Major Section:  DEFUN-SK

The symbol forall (in the ACL2 package) represents universal quantification in the context of a defun-sk form. See defun-sk and see exists.













































































ENCAPSULATE

constrain some functions and/or hide some events
Major Section:  EVENTS

Examples:
(encapsulate ((an-element (lst) t))
  (local (defun an-element (lst)
           (if (consp lst) (car lst) nil)))
  (local (defthm member-equal-car
            (implies (and lst (true-listp lst))
                     (member-equal (car lst) lst))))
  (defthm thm1
     (implies (null lst) (null (an-element lst))))
  (defthm thm2
     (implies (and (true-listp lst)
                   (not (null lst)))
              (member-equal (an-element lst) lst))))

(encapsulate ()

(local (defthm hack (implies (and (syntaxp (quotep x)) (syntaxp (quotep y))) (equal (+ x y z) (+ (+ x y) z)))))

(defthm nthcdr-add1-conditional (implies (not (zp (1+ n))) (equal (nthcdr (1+ n) x) (nthcdr n (cdr x))))))

General Form: (encapsulate (signature ... signature) ev1 ... evn)

where each signature is as described in the documentation for signature, each signature describes a different function symbol, and each evi is an embedded event form as described in the documentation for embedded-event-form. There must be at least one evi. The evi inside local special forms are called ``local'' events below. Events that are not local are sometimes said to be ``exported'' by the encapsulation. We make the further restriction that no defaxiom event may be introduced in the scope of an encapsulate (not even by encapsulate or include-book events that are among the evi). Furthermore, no non-local include-book event is permitted in the scope of any encapsulate with a non-empty list of signatures.

To be well-formed, an encapsulate event must have the properties that each event in the body (including the local ones) can be successfully executed in sequence and that in the resulting theory, each function mentioned among the signatures was introduced via a local event and has the signature listed. In addition, the body may contain no ``local incompatibilities'' which, roughly stated, means that the events that are not local must not syntactically require symbols defined by local events, except for the functions listed in the signatures. See local-incompatibility. Finally, no non-local recursive definition in the body may involve in its suggested induction scheme any function symbol listed among the signatures. See subversive-inductions.

The result of an encapsulate event is an extension of the logic in which, roughly speaking, the functions listed in the signatures are constrained to have the signatures listed and to satisfy the non-local theorems proved about them. In fact, other functions introduced in the encapsulate event may be considered to have ``constraints'' as well. (See constraint for details, which are only relevant to functional instantiation.) Since the constraints were all theorems in the ``ephemeral'' or ``local'' theory, we are assured that the extension produced by encapsulate is sound. In essence, the local definitions of the constrained functions are just ``witness functions'' that establish the consistency of the constraints. Because those definitions are local, they are not present in the theory produced by encapsulation. Encapsulate also exports all rules generated by its non-local events, but rules generated by local events are not exported.

The default-defun-mode for the first event in an encapsulation is the default defun-mode ``outside'' the encapsulation. But since events changing the defun-mode are permitted within the body of an encapsulate, the default defun-mode may be changed. However, defun-mode changes occurring within the body of the encapsulate are not exported. In particular, the acl2-defaults-table after an encapsulate is always the same as it was before the encapsulate, even though the encapsulate body might contain defun-mode changing events, :program and :logic. See defun-mode. More generally, after execution of an encapsulate event, the value of acl2-defaults-table is restored to what it was immediately before that event was executed. See acl2-defaults-table.

Theorems about the constrained function symbols may then be proved -- theorems whose proofs necessarily employ only the constraints. Thus, those theorems may be later functionally instantiated, as with the :functional-instance lemma instance (see lemma-instance), to derive analogous theorems about different functions, provided the constraints (see constraint) can be proved about the new functions.

Observe that if the signatures list is empty, encapsulate may still be useful for deriving theorems to be exported whose proofs require lemmas you prefer to hide (i.e., made local).

The order of the events in the vicinity of an encapsulate is confusing. We discuss it in some detail here because when logical names are being used with theory functions to compute sets of rules, it is sometimes important to know the order in which events were executed. (See logical-name and see theory-functions.) What, for example, is the set of function names extant in the middle of an encapsulation?

If the most recent event is previous and then you execute an encapsulate constraining an-element with two non-local events in its body, thm1 and thm2, then the order of the events after the encapsulation is (reading chronologically forward): previous, thm1, thm2, an-element (the encapsulate itself). Actually, between previous and thm1 certain extensions were made to the world by the superior encapsulate, to permit an-element to be used as a function symbol in thm1.

Finally, we note that an encapsulate event is redundant if and only if a syntactically identical encapsulate has already been executed under the same default-defun-mode. See redundant-events.













































































IN-THEORY

designate ``current'' theory (enabling its rules)
Major Section:  EVENTS

Example:
(in-theory (set-difference-theories
             (universal-theory :here)
             '(flatten (:executable-counterpart flatten))))

General Form: (in-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see theories), and doc-string is an optional documentation string not beginning with ``:doc-section ...''. Except for the variable world, term must contain no free variables. Term is evaluated with the variable world bound to the current world to obtain a theory and the corresponding runic theory (see theories) is then made the current theory. Thus, immediately after the in-theory, a rule is enabled iff its rule name is a member of the runic interpretation (see theories) of some member of the value of term. See theory-functions for a list of the commonly used theory manipulation functions.

Because no unique name is associated with an in-theory event, there is no way we can store the documentation string doc-string in our documentation data base. Hence, we actually prohibit doc-string from having the form of an ACL2 documentation string; see doc-string.













































































INCLUDE-BOOK

load the events in a file
Major Section:  EVENTS

Examples:
(include-book "my-arith")
(include-book (:RELATIVE "my-arith"))
(include-book "/home/smith/my-arith")
(include-book (:ABSOLUTE "home" "smith" "my-arith"))

General Form: (include-book file :load-compiled-file action :doc doc-string)

where file is a book name. See books for general information, see book-name for information about book names, and see pathname for information about file names (including structured pathnames). Action is one of t, nil, :warn (the default), or :try; these values are explained below. Doc-string is an optional documentation string; see doc-string. If the book has no certificate, if its certificate is invalid or if the certificate was produced by a different version of ACL2, a warning is printed and the book is included anyway; see certificate. This can lead to serious errors; see uncertified-books. If the portcullis of the certificate (see portcullis) cannot be raised in the host logical world, an error is caused and no change occurs to the logic. Otherwise, the non-local events in file are assumed. Then the keep of the certificate is checked to insure that the correct files were read; see keep. A warning is printed if uncertified books were included. Even if no warning is printed, include-book places a burden on you; see certificate.

If there is a compiled file for the book that was created more recently than the book itself and the value action of the :load-compiled-file argument is not nil, or is omitted, then the compiled file is automatically loaded; otherwise it is not loaded. If action is t then the compiled file must be loaded or an error will occur, while if action is :warn (the default) then a warning will be printed. Certify-book can be used to compile a book. The effect of compilation is to speed up the execution of the functions defined within the book when those functions are applied to specific values. The presence of compiled code for the functions in the book should not otherwise affect the performance of ACL2. See guard for a discussion.

Include-book is similar in spirit to encapsulate in that it is a single event that ``contains'' other events, in this case the events listed in the file named. Include-book processes the non-local event forms in the file, assuming that each is admissible. Local events in the file are ignored. You may use include-book to load multiple books, creating the logical world that contains the definitions and theorems of all of them.

If any non-local event of the book attempts to define a name that has already been defined -- and the book's definition is not syntactically identical to the existing definition -- the attempt to include the book fails, an error message is printed, and no change to the logical world occurs. See redundant-events for the details.

When a book is included, the default defun-mode (see default-defun-mode) for the first event is always :logic. That is, the default defun-mode ``outside'' the book -- in the environment in which include-book was called -- is irrelevant to the book. Events that change the defun-mode are permitted within a book (provided they are not in local forms). However, such changes within a book are not exported, i.e., at the conclusion of an include-book, the ``outside'' default defun-mode is always the same as it was before the include-book.

Unlike every other event in ACL2, include-book puts a burden on you. Used improperly, include-book can be unsound in the sense that it can create an inconsistent extension of a consistent logical world. A certification mechanism is available to help you carry this burden -- but it must be understood up front that even certification is no guarantee against inconsistency here. The fundamental problem is one of file system security. See certificate for a discussion of the security issues.

After execution of an include-book form, the value of acl2-defaults-table is restored to what it was immediately before that include-book form was executed. See acl2-defaults-table.

This concludes the guided tour through books. See set-compile-fns for a subtle point about the interaction between include-book and on-the-fly compilation. See certify-book for a discussion of how to certify a book.













































































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.













































































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-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.













































































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.