• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
      • Miscellaneous
      • Output-controls
      • Bdd
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Macro-libraries
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • 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
      • Installation
      • Mailing-lists
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • ACL2

Macros

Macros allow you to extend the syntax of ACL2.

Subtopics

Make-event
Evaluate (expand) a given form and then evaluate the result
Defmacro
Define a macro
Untranslate-patterns
A database used to extend untranslate, ACL2's function for displaying terms during proofs, with pattern-based rules.
Tc
translate form and clean it up
Trans*
Show intermediate expansion results for the translation of a form
Macro-aliases-table
A table used to associate function names with macro names
Macro-args
The formals list of a macro definition
Defabbrev
A convenient form of macro definition for simple expansions
User-defined-functions-table
An advanced table used to replace certain system functions
Trans
Print the translation of a form
Untranslate-for-execution
Attempt to do a kind of untranslation of a ute-term-p in order to restore any mv-let and mv forms, ideally so that the term can be executed.
Macro-libraries
Libraries of useful macros
Add-macro-fn
Associate a function name with a macro name
Check-vars-not-free
Avoid variable capture in macro calls
Safe-mode
A mode that avoids guard violations on primitives
Trans1
Print the one-step macroexpansion of a form
Defmacro-untouchable
Define an ``untouchable'' macro
Set-duplicate-keys-action
Control action for macro calls with duplicate keyword arguments
Add-macro-alias
Associate a function name with a macro name
Magic-macroexpand
A macroexpansion utility for logic-mode code
Defmacroq
Define a macro that quotes arguments not wrapped in :eval
Trans!
Print the translation of a form without code restrictions
Remove-macro-fn
Remove the association of a function name with a macro name
Remove-macro-alias
Remove the association of a function name with a macro name
Add-binop
Associate a function name with a macro name
Untrans-table
Associates a function symbol with a macro for printing user-level terms
Trans*-
Variant of trans* the skips make-event expansion
Remove-binop
Remove the association of a function name with a macro name
Tcp
translate a form and clean it up into a pretty term
Tca
translate a form and clean it up into an annotated pretty term