## 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))))
```

• ### FORALL -- universal quantifier

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

(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 `defun`s 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 `defun`s.

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 `ignore`d. 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`.