Macro-libraries
Libraries of useful macros
See macros for documentation of macros that are built into
ACL2.
The subtopics below describe macros defined in the community-books
that support writing more concise code, including frameworks for quickly
introducing concepts like typed structures, typed lists, defining functions
with type signatures, and automating other common tasks.
Subtopics
- B*
- The b* macro is a replacement for let* that adds support
for multiple return values, mixing control flow with binding, causing side
effects, introducing type declarations, and doing other kinds of custom pattern
matching.
- Defunc
- Function definitions with contracts. See also
definec and defun.
- Fty
- FTY is a macro library for introducing new data types and writing
type-safe programs in ACL2. It automates a systematic discipline for working
with types that allows for both efficient reasoning and execution.
- Apt
- APT (Automated Program Transformations) is a library of tools
to transform programs and program specifications
with automated support.
- Std/util
- A macro library that automates defining types, introducing typed
functions, mapping over lists, and many other boilerplate tasks.
- Defdata
- A Data Definition Framework
- Defrstobj
- Record-like stobjs combine the run-time efficiency of stobjs
with the reasoning efficiency of records. They are designed for modeling,
e.g., the state of a processor or virtual machine.
- Seq
- Seq is a macro language for applying actions to a stream.
- Match-tree
- Match an object against a flexible pattern and return the unifying substitution
- Defrstobj
- Record-like stobjs combine the run-time efficiency of stobjs
with the reasoning efficiency of records. They are designed for modeling,
e.g., the state of a processor or virtual machine.
- With-supporters
- Automatically include specified definitions from a specified book
- Def-partial-measure
- Introduce measure and termination predicates for a partial function
definition
- Template-subst
- Template-subst is a function for manipulating templates that may be
used to generate events.
- Soft
- SOFT (Second-Order Functions and Theorems)
is a tool to mimic second-order functions and theorems
in the first-order logic of ACL2.
- Defthm-domain
- Prove termination on a given domain
- Event-macros
- A library of concepts and utilities for event macros.
- Def-universal-equiv
- A macro for defining universally quantified equivalence relations.
- Def-saved-obligs
- Save the proof obligations for a given event as separate defthms.
- With-supporters-after
- Automatically define necessary redundant definitions from after a
specified event
- Definec
- Function definitions with contracts extending defunc.
- Sig
- Specify type signatures for polymorphic functions
- Outer-local
- Support for events that are local to the outer context.
- Data-structures
- The books/data-structures library
