Std/util
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.
Subtopics
- 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
with XDOC 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.
