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.
- Error-value-tuples
- Utilities for error-value tuples.
- 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.
- Defsurj
- Establish a surjective mapping between two domains.
- Defiso
- Establish an isomorphic mapping between two domains.
- Defund-sk
- Define a function with quantifier
and disable it and its associated rewrite rule.
- Defthm-commutative
- Introduce a commutativity theorem.
- Definj
- Establish an injective mapping between two domains.