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

    Add-binop

    Associate a function name with a macro name

    The form (add-binop macro macro-fn) is an abbreviation for the form (add-macro-fn macro macro-fn t). See add-macro-fn.