INVISIBLE-FNS-ALIST

functions that are invisible to the loop-stopper algorithm 
Major Section:  MISCELLANEOUS


Examples:
ACL2 !>(invisible-fns-alist (w state))
((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. See set-invisible-fns-alist.

The notion of ``invisible functions'' has to do with the control mechanism on permutative :rewrite rules. See loop-stopper for a detailed discussion of the control mechanism. See set-invisible-fns-alist for a discussion of how to set the invisible functions alist.