Std/util-extensions
Extensions of Std/util in the Kestrel Books.
These extensions could be moved under std/util
at some point.
Subtopics
- Defmapping
- Establish a mapping between two domains.
- Defarbrec
- Introduce an arbitrarily recursive function.
- Defmax-nat
- Declaratively define the maximum of a set of natural numbers.
- Error-value-tuples
- Utilities for error-value tuples.
- Defmin-int
- Declaratively define the minimum of a set of integer numbers.
- Deftutorial
- Generate utilities to build a tutorial.
- 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.
- Defund-sk
- Define a function with quantifier
and disable it and its associated rewrite rule.
- Defmacro+
- An enhancement of defmacro
with XDOC integration.
- Defthm-commutative
- Introduce a commutativity theorem.
- Definj
- Establish an injective mapping between two domains.
- Defirrelevant
- Define an irrelevant value of a type.
