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.