Extensions of Std/util in the Kestrel Books.
These extensions could be moved under [books]/std/util
at some point.
- Establish a mapping between two domains.
- Introduce an arbitrarily recursive function.
- Declaratively define the maximum of a set of natural numbers.
- Declaratively define the minimum of a set of integer numbers.
- Generate utilities to build a tutorial.
- Establish a surjective mapping between two domains.
- Establish an isomorphic mapping between two domains.
- Introduce a constrained recognizer.
- Introduce a fixer for a predicate.
- Define a function with quantifier
and disable it and its associated rewrite rule.
- An enhancement of defmacro
with XDOC integration.
- Introduce a commutativity theorem.
- Establish an injective mapping between two domains.