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.