• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
          • Force
          • Hide
          • Syntaxp
          • Free-variables
          • Bind-free
          • Loop-stopper
            • Invisible-fns-table
            • Set-invisible-fns-table
            • Add-invisible-fns
            • Remove-invisible-fns
            • Backchain-limit
            • Double-rewrite
            • Rewrite-lambda-object
            • Rewriting-versus-cleaning-up-lambda-objects
            • Random-remarks-on-rewriting
            • Set-rw-cache-state
            • Case-split
            • Rewrite-lambda-object-actions
            • Syntactically-clean-lambda-objects-theory
            • Hands-off-lambda-objects-theory
            • Rewrite-lambda-objects-theory
            • Simple
            • Rewrite-stack-limit
            • Rewrite-equiv
            • Assume-true-false-aggressive-p
            • Remove-trivial-equivalences-enabled-p
            • Rewrite-lambda-modep
            • Rewrite-if-avoid-swap
            • Set-rw-cache-state!
            • Rw-cache-state
          • Meta
          • Linear
          • Definition
          • Clause-processor
          • Tau-system
          • Forward-chaining
          • Equivalence
          • Congruence
          • Free-variables
          • Executable-counterpart
          • Induction
          • Type-reasoning
          • Compound-recognizer
          • Rewrite-quoted-constant
          • Elim
          • Well-founded-relation-rule
          • Built-in-clause
          • Well-formedness-guarantee
          • Patterned-congruence
          • Rule-classes-introduction
          • Guard-holders
          • Refinement
          • Type-set-inverter
          • Generalize
          • Corollary
          • Induction-heuristics
          • Backchaining
          • Default-backchain-limit
        • Proof-builder
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Loop-stopper

    Remove-invisible-fns

    Make some unary functions no longer invisible

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

    The setting above has makes unary functions unary-- and foo no longer ``invisible'' for the purposes of applying permutative :rewrite rules to binary-+ trees.

    General Form:
    (remove-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).

    See add-invisible-fns and also see invisible-fns-table and see set-invisible-fns-table.