Reserr
Fixtype of error results.
This is a product type introduced by defprod.
Fields
- info — ACL2::any-p
This is the fixtype of error results for defresult;
see the introduction of defresult for background and motivation.
An error result consists of some unconstrained information,
wrapped with :error to make it distinct from any good value
(assuming that good values do not have the form (:error ...),
a condition that seems reasonably easy to satisfy).
Subtopics
- Reserrp
- Recognizer for reserr structures.
- Reserr-fix
- Fixing function for reserr structures.
- Reserr-equiv
- Basic equivalence relation for reserr structures.
- Make-reserr
- Basic constructor macro for reserr structures.
- Change-reserr
- Modifying constructor for reserr structures.
- Reserr->info
- Get the info field from a reserr.
