Kestrel-utilities
Utilities that are part of the
Kestrel Books.
Subtopics
- 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
- Numbered-names
- Utilities for numbered names.
- Context-message-pair
- A common ACL2 programming idiom: error-triples without state
- 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.
- Ubi
- Undo back up to longest initial segment containing only calls of
certain symbols, including defpkg and include-book.
- 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
- Checkpoint-list
- Return prover key checkpoint clauses programmatically.
- Defthm<w
- Attempt to prove a theorem directly from previously-proved theorems.
- System-utilities-non-built-in
- System utilities related to the ACL2 system.
- Prove$
- A way to call the prover from a program
- Integer-range-fix
- Fixing function for integer-range-p.
- Integers-from-to
- Ordered list of all the integers in a range.
- Minimize-ruler-extenders
- Minimize the ruler-extenders necessary to admit a definition.
- Add-const-to-untranslate-preprocess
- Extend untranslate-preprocess
to keep a constant unexpanded in output.
- 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.
- 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.
- Checkpoint-list-pretty
- Return prover key checkpoint goals programmatically.
- 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.
- 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.
