Expdata-surjmapp
Information about a surjective mapping according to which
(some of) the target function's arguments and results
are transformed.
(expdata-surjmapp x) is a std::defaggregate of the following fields.
- surjname — Name of the defsurj.
Invariant (symbolp surjname).
- localp — Flag saying whether the defsurj is
locally generated or not.
Invariant (booleanp localp).
- oldp — Recognizer of the old representation,
i.e. the domb domain of the defsurj.
Invariant (pseudo-termfnp oldp).
- newp — Recognizer of the new representation,
i.e. the doma domain of the defsurj.
Invariant (pseudo-termfnp newp).
- forth — Conversion from old to new representation,
i.e. the beta conversion of the defsurj.
Invariant (pseudo-termfnp forth).
- back — Conversion from new to old representation,
i.e. the alpha conversion of the defsurj.
Invariant (pseudo-termfnp back).
- forth-image — Name of the :beta-image theorem of the defsurj.
Invariant (symbolp forth-image).
- back-image — Name of the :alpha-image theorem of the defsurj.
Invariant (symbolp back-image).
- back-of-forth — Name of the :alpha-of-beta theorem
of the defsurj.
Invariant (symbolp back-of-forth).
- forth-injective — Name of the :beta-injective theorem
of the defsurj.
Invariant (symbolp forth-injective).
- oldp-guard — Name of the :domb-guard theorem
of the defsurj, if present (otherwise nil).
Invariant (symbolp oldp-guard).
- newp-guard — Name of the :doma-guard theorem
of the defsurj, if present (otherwise nil).
Invariant (symbolp newp-guard).
- forth-guard — Name of the :beta-guard theorem
of the defsurj, if present (otherwise nil).
Invariant (symbolp forth-guard).
- back-guard — Name of the :alpha-guard theorem
of the defsurj, if present (otherwise nil).
Invariant (symbolp back-guard).
- hints — Optional hints for the defsurj,
if locally generated (otherwise nil).
Invariant (keyword-value-listp hints).
Source link: expdata-surjmapp
This aggregate is somewhat similar to defmapping-infop,
and in fact it corresponds
either to an existing defsurj that is referenced
in an surjk input of expdata,
or to a locally generated defsurj that is determined
in the surjk input of expdata.
However, this aggregate is not stored in any table;
it has some fields in common (except for their names)
with defmapping-infop,
but it has a few extra fields and omits a few fields.
This aggregate is only for expdata's internal use.
Note that there are no forth-of-back and back-injective theorems,
because the corresponding theorems are not in the defsurj.
Subtopics
- Expdata-surjmap
- Raw constructor for expdata-surjmapp structures.
- Make-expdata-surjmap
- Constructor macro for expdata-surjmapp structures.
- Change-expdata-surjmap
- A copying macro that lets you create new expdata-surjmapp structures, based on existing structures.
- Honsed-expdata-surjmap
- Raw constructor for honsed expdata-surjmapp structures.
- Make-honsed-expdata-surjmap
- Constructor macro for honsed expdata-surjmapp structures.
- Expdata-surjmap->surjname
- Access the surjname field of a expdata-surjmapp structure.
- Expdata-surjmap->oldp-guard
- Access the oldp-guard field of a expdata-surjmapp structure.
- Expdata-surjmap->oldp
- Access the oldp field of a expdata-surjmapp structure.
- Expdata-surjmap->newp-guard
- Access the newp-guard field of a expdata-surjmapp structure.
- Expdata-surjmap->newp
- Access the newp field of a expdata-surjmapp structure.
- Expdata-surjmap->localp
- Access the localp field of a expdata-surjmapp structure.
- Expdata-surjmap->hints
- Access the hints field of a expdata-surjmapp structure.
- Expdata-surjmap->forth-injective
- Access the forth-injective field of a expdata-surjmapp structure.
- Expdata-surjmap->forth-image
- Access the forth-image field of a expdata-surjmapp structure.
- Expdata-surjmap->forth-guard
- Access the forth-guard field of a expdata-surjmapp structure.
- Expdata-surjmap->forth
- Access the forth field of a expdata-surjmapp structure.
- Expdata-surjmap->back-of-forth
- Access the back-of-forth field of a expdata-surjmapp structure.
- Expdata-surjmap->back-image
- Access the back-image field of a expdata-surjmapp structure.
- Expdata-surjmap->back-guard
- Access the back-guard field of a expdata-surjmapp structure.
- Expdata-surjmap->back
- Access the back field of a expdata-surjmapp structure.
