Search-engine friendly clone of the
ACL2 documentation
.
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
primitive
s
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