		Search-engine friendly clone of the ACL2 documentation.

Loop-stopper

Add-invisible-fns

Make some unary functions invisible to the loop-stopper algorithm

Examples:
(add-invisible-fns binary-+ unary-- foo)
(add-invisible-fns + unary-- foo)

Each of the events above makes unary functions unary-- and foo ``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.

General Form:
(add-invisible-fns top-fn unary-fn1 ... unary-fnk)

where top-fn is a function symbol and the unary-fni are unary function symbols, or more generally, these are all macro aliases for such function symbols (see macro-aliases-table).

For more information see invisible-fns-table. Also see set-invisible-fns-table, which explains how to set the entire table in a single event, and see remove-invisible-fns.