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)
- simple enumerations (defenum),
- record types like
struct s in C (defaggregate), - (beta) tagged union / variant / sum types (defsum),
- typed lists (deflist), and
- typed alists (defalist)

- Projecting a function across a list and either
- cons the results together (defprojection), or
- append the results (defmapappend).

- Defining functions with documentation and related theorems (define)
- Writing mutually-recursive functions with induction schemes (defines)
- Automating other tedious tasks
:type-prescription s formv -returning functions (defmvtypes)- defining simple constants with xdoc documentation (defval)
- defining constants that depend on stobjs, with
mv support (defconsts) - proving rewrite, type prescription, and linear rules about terms in
`natp`,`unsigned-byte-p`, and`signed-byte-p`.

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

- Defprojection
- Project a transformation across a list.
- Deflist
- Introduce a recognizer for a typed list.
- Defaggregate
- Introduce a record structure, like a
struct in C. - Define
- A very fine alternative to defun.
- Defmapping
- Establish a mapping between two domains.
- Defenum
- Introduce an enumeration type, like an
enum in C. - Add-io-pairs
- Speed up a function using verified input-output pairs
- Defalist
- Introduce a recognizer for a typed association list (alist).
- Defmapappend
- Append transformations of list elements.
- Returns-specifiers
- A concise way to name, document, and prove basic type-like theorems about a function's return values.
- Defarbrec
- Introduce an arbitrarily recursive function.
- Define-sk
- A very fine alternative to
`defun-sk`. - Error-value-tuples
- Utilities for error-value tuples.
- Defines
- A very fine alternative to mutual-recursion.
- Defmax-nat
- Declaratively define the maximum of a set of natural numbers.
- Defmin-int
- Declaratively define the minimum of a set of integer numbers.
- Deftutorial
- Generate utilities to build a tutorial.
- Extended-formals
- Extended syntax for function arguments that allows for built-in guards, documentation, and macro-like keyword/optional arguments.
- Defrule
- An enhanced version of defthm.
- Defval
- A replacement for defconst with xdoc integration.
- Defsurj
- Establish a surjective mapping between two domains.
- Defiso
- Establish an isomorphic mapping between two domains.
- Defconstrained-recognizer
- Introduce a constrained recognizer.
- Deffixer
- Introduce a fixer for a predicate.
- Defmvtypes
- Introduce type-prescription rules for a function that returns multiple values.
- Defconsts
- 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.
- Support
- Miscellaneous supporting functions used by the std/util library.
- Defthm-signed-byte-p
- Prove rules about a term yielding values in
`signed-byte-p`. - Defthm-unsigned-byte-p
- Prove rules about a term yielding values in
`unsigned-byte-p`. - Defthm-natp
- Prove rules about a term yielding values in
`natp`. - Defund-sk
- Define a function with quantifier and disable it and its associated rewrite rule.
- Defmacro+
- An enhancement of
`defmacro`withXDOC integration. - Defsum
- (Beta) Introduce a tagged union data type, also commonly called a variant or sum type.
- Defthm-commutative
- Introduce a commutativity theorem.
- Definj
- Establish an injective mapping between two domains.
- Defirrelevant
- Define an irrelevant value of a type.
- Defredundant
- A macro for automatically introducing ACL2::redundant-events, which is useful for developing "interface" books and otherwise avoiding copying and pasting code.