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.
- 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.
- 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
