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