Utilities that are part of the

- Omaps
- A library of omaps (ordered maps), i.e. finite maps represented as strictly ordered alists.
- Directed-untranslate
- Create a user-level form that reflects a given user-level form's structure.
- Include-book-paths
- List paths via
`include-book`down to a given book - Ubi
- Undo back up to longest initial segment containing only calls of
certain symbols, including
`defpkg`and`include-book`. - Checkpoint-list
- Return prover key checkpoint clauses programmatically.
- Context-message-pair
- A common ACL2 programming idiom: error-triples without state
- Numbered-names
- Utilities for numbered names.
- With-auto-termination
- Re-use an existing termination proof automatically.
- Digits-any-base
- Conversions between natural numbers and their representations as digits in arbitrary bases.
- Make-termination-theorem
- Create a copy of a function's termination theorem that calls stubs.
- Sublis-expr+
- Replace terms by variables, even inside lambda bodies
- Prove$
- A way to call the prover from a program
- Defthm<w
- Attempt to prove a theorem directly from previously-proved theorems.
- System-utilities-non-built-in
- System utilities related to the ACL2 system.
- Integer-range-fix
- Fixing function for
`integer-range-p`. - Add-const-to-untranslate-preprocess
- Extend
`untranslate-preprocess`to keep a constant unexpanded in output. - Integers-from-to
- Ordered list of all the integers in a range.
- Minimize-ruler-extenders
- Minimize the ruler-extenders necessary to admit a definition.
- Unsigned-byte-fix
- Fixing function for
`unsigned-byte-p`. - Signed-byte-fix
- Fixing function for
`signed-byte-p`. - Defthmr
- Submit a theorem, as a rewrite rule only if possible.
- Paired-names
- Utilities for paired names.
- Unsigned-byte-list-fix
- Fixing function for
`unsigned-byte-listp`. - Signed-byte-list-fix
- Fixing function for
`signed-byte-listp`. - Checkpoint-list-pretty
- Return prover key checkpoint goals programmatically.
- List-utilities
- Some utilities for lists.
- Skip-in-book
- Skip a form when executing
`certify-book`or`include-book` - Typed-tuplep
- Recognize typed tuples, i.e. true lists whose elements satisfy specified predicates.
- Defunt
- Variant of
`defun`that re-uses existing termination theorems automatically. - Keyword-value-list-to-alist
- Turn a true list of even length with keywords at its even-numbered positions (counting from 0), into the corresponding alist.
- Magic-macroexpand
- A macroexpansion utility for logic-mode code
- Top-command-number-fn
- Returns the number of the most recent top-level ACL2 command.
- Bits-as-digits-in-base-2
- Specialized versions of the operations to convert between natural numbers and digits that use bits as digits, in base 2.
- Show-checkpoint-list
- Display prover key checkpoint information.
- Ubyte11s-as-digits-in-base-2048
- Specialized versions of the operations to convert between natural numbers and digits that use unsigned 11-bit bytes as digits, in base 2048.
- Named-formulas
- Utilities for named formulas.
- Bytes-as-digits-in-base-256
- Specialized versions of the operations to convert between natural numbers and digits that use bytes as digits, in base 256.
- String-utilities
- Some utilities for strings (and characters).
- Make-keyword-value-list-from-keys-and-value
- Make a list satisfying
`keyword-value-listp`by associating each member of a true-list of keywords list of keywords with a given value. - Integer-range-listp
- Recognize true lists of integers in ranges.
- Defmacroq
- Define a macro that quotes arguments not wrapped in
:eval - Apply-fn-if-known
- Apply a function, expressed as a package and a name, if it exists.
- Trans-eval-error-triple
- An ACL2 evaluator for forms that return error-triples
- Checkpoint-info-list
- Return prover key checkpoint information programmatically.
- Previous-subsumer-hints
- Hints to prove a theorem directly from previously-proved theorems.
- Fms!-lst
- Write each object in a list to a character output channel.
- Zp-listp
- Recognize true lists of
`zp`values. - Doublets-to-alist
- Turn a true list of doublets (i.e. lists of length 2) into the corresponding alist.
- Trans-eval-state
- An ACL2 evaluator that returns state
- Injections
- Set of all functions from a finite domain to a finite range
- Typed-list-utilities
- Some utilities for typed lists.
- Book-runes-alist
- Returns an alist associating book full pathnames with runes introduced
- User-interface
- Utilities for the user interface of event-generating macros (e.g. program transformations).
- Bits/ubyte11s-digit-grouping
- Specialized versions of the operations to group and ungroup digitsthat are bits (base 2) and unsigned 11-bit bytes (base 2048).
- Bits/bytes-digit-grouping
- Specialized versions of the operations to group and ungroup digitsthat are bits (base 2) and bytes (base 256).
- Message-utilities
- Utilities for
messages. - Subsetp-eq-linear
- A linear-time subset test for sorted lists of symbols
- Strict-merge-sort-<
- Sort a list of rational numbers into
< -increasing order - Miscellaneous-enumerations
- Some miscellaneous enumerations.
- Maybe-unquote
- Unquote an object, if quoted; otherwise, leave unchanged.
- Oset-utilities
- Utilities for
finite sets. - Thm<w
- Attempt to prove a theorem directly from previously-proved theorems.
- Theorems-about-non-kestrel-books
- Theorems about functions defined outside the
Kestrel Books. - Defthmd<w
- Attempt to prove a theorem directly from previously-proved theorems.