• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • Macro-libraries
        • Trans1
        • Defmacro-untouchable
        • Set-duplicate-keys-action
        • Add-macro-alias
        • Magic-macroexpand
        • Defmacroq
        • Trans!
        • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Macros

    Remove-macro-fn

    Remove the association of a function name with a macro name

    Example:
    (remove-macro-fn binary-append)
    
    General Form:
    (remove-macro-fn macro-fn)

    See add-macro-fn for a discussion of how to associate a macro name with a function name. This form sets untrans-table to the result of deleting the association of a macro name with the given binary function name. If the function name has no such association, then this form still generates an event, but the event has no real effect.