• 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

    Add-macro-alias

    Associate a function name with a macro name

    Example:
    (add-macro-alias append binary-append)

    This example associates the function symbol binary-append with the macro name append. As a result, the name append may be used as a runic designator (see theories) by the various theory functions. See macro-aliases-table for more details. Also see add-macro-fn for an extension of this utility that also affects printing.

    General Form:
    (add-macro-alias macro-name function-name)

    This is a convenient way to add an entry to macro-aliases-table. See macro-aliases-table and also see remove-macro-alias.