		Search-engine friendly clone of the ACL2 documentation.

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.
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
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.
Trans: Print the macroexpansion of a form
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
Macro-libraries: Generally useful macros for writing more concise code, and frameworks for quickly introducing concepts like typed structures, typed lists, defining functions with type signatures, and automating other common tasks.
Defmacro-untouchable: Define an ``untouchable'' macro
Trans1: Print the one-step macroexpansion of a form
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
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!: Print the macroexpansion of a form without single-threadedness concerns
Remove-binop: Remove the association of a function name with a macro name