A macro library that automates defining types, introducing typed
functions, mapping over lists, and many other boilerplate tasks.
We provide macros for
- Introducing data types (recognizers and basic theorems)
- Projecting a function across a list and either
- Defining functions with documentation and related theorems (define)
- Writing mutually-recursive functions with induction schemes (defines)
- Automating other tedious tasks
Loading the library
You can load the full library with:
(include-book "std/util/top" :dir :system)
Alternately, you may find it convenient to just load individual books. Each
major macro is typically defined in its own book, e.g., you could do:
(include-book "std/util/define" :dir :system)
(include-book "std/util/defaggregate" :dir :system)
(include-book "std/util/deflist" :dir :system)
Note that unlike many other std libraries, these macros are defined
in the STD:: package. This is mainly to avoid name collisions with older
macros like deflist from other libraries.
- Project a transformation across a list.
- Introduce a recognizer for a typed list.
- Introduce a record structure, like a struct in C.
- A very fine alternative to defun.
- Establish a mapping between two domains.
- Introduce an enumeration type, like an enum in C.
- Speed up a function using verified input-output pairs
- Introduce a recognizer for a typed association list (alist).
- Append transformations of list elements.
- Introduce an arbitrarily recursive function.
- A concise way to name, document, and prove basic type-like theorems
about a function's return values.
- A very fine alternative to defun-sk.
- Declaratively define the maximum of a set of natural numbers.
- A very fine alternative to mutual-recursion.
- Utilities for error-value tuples.
- Declaratively define the minimum of a set of integer numbers.
- Generate utilities to build a tutorial.
- Extended syntax for function arguments that allows for built-in
guards, documentation, and macro-like keyword/optional arguments.
- An enhanced version of defthm.
- A replacement for defconst with xdoc integration.
- Establish a surjective mapping between two domains.
- Establish an isomorphic mapping between two domains.
- Introduce a constrained recognizer.
- Introduce a fixer for a predicate.
- Introduce type-prescription rules for a function that returns
- An enhanced variant of defconst that lets you use state
and other ACL2::stobjs, and directly supports calling mv-returning functions to define multiple constants.
- Miscellaneous supporting functions used by the std/util library.
- Prove rules about a term yielding values in signed-byte-p.
- Prove rules about a term yielding values in unsigned-byte-p.
- Extensions of Std/util in the Kestrel Books.
- Prove rules about a term yielding values in natp.
- Define a function with quantifier
and disable it and its associated rewrite rule.
- An enhancement of defmacro
with XDOC integration.
- (Beta) Introduce a tagged union data type, also commonly called a
variant or sum type.
- Introduce a commutativity theorem.
- Establish an injective mapping between two domains.
- Define an irrelevant value of a type.
- A macro for automatically introducing ACL2::redundant-events,
which is useful for developing "interface" books and otherwise avoiding
copying and pasting code.