Defmapping-infop
Information about a defmapping call,
recorded as a pair's value in the defmapping table.
(defmapping-infop x) is a std::defaggregate of the following fields.
- call$ — The call to defmapping,
without :print and :show-only.
Invariant (pseudo-event-formp call$).
- expansion — The encapsulate generated from
the call to defmapping.
Invariant (pseudo-event-formp expansion).
- doma — Domain A, in translated form.
Invariant (pseudo-termfnp doma).
- domb — Domain B, in translated form.
Invariant (pseudo-termfnp domb).
- alpha — Conversion \alpha, in translated form.
Invariant (pseudo-termfnp alpha).
- beta — Conversion \beta, in translated form.
Invariant (pseudo-termfnp beta).
- alpha-image — Name of the :alpha-image theorem.
Invariant (symbolp alpha-image).
- beta-image — Name of the :beta-image theorem.
Invariant (symbolp beta-image).
- beta-of-alpha — Name of the :beta-of-alpha theorem, if present (otherwise nil.
Invariant (symbolp beta-of-alpha).
- alpha-of-beta — Name of the :alpha-of-beta theorem, if present (otherwise nil.
Invariant (symbolp alpha-of-beta).
- alpha-injective — Name of the :alpha-injective theorem, if present (otherwise nil.
Invariant (symbolp alpha-injective).
- beta-injective — Name of the :beta-injective theorem, if present (otherwise nil.
Invariant (symbolp beta-injective).
- doma-guard — Name of the :doma-guard theorem, if present (otherwise nil).
Invariant (symbolp doma-guard).
- domb-guard — Name of the :domb-guard theorem, if present (otherwise nil).
Invariant (symbolp domb-guard).
- alpha-guard — Name of the :alpha-guard theorem, if present (otherwise nil).
Invariant (symbolp alpha-guard).
- beta-guard — Name of the :beta-guard theorem, if present (otherwise nil).
Invariant (symbolp beta-guard).
- unconditional — Value of the :unconditional input,
i.e. whether some of the theorems
are unconditional or not.
Invariant (booleanp unconditional).
Source link: defmapping-infop
Subtopics
- Defmapping-info
- Raw constructor for defmapping-infop structures.
- Make-defmapping-info
- Constructor macro for defmapping-infop structures.
- Change-defmapping-info
- A copying macro that lets you create new defmapping-infop structures, based on existing structures.
- Honsed-defmapping-info
- Raw constructor for honsed defmapping-infop structures.
- Make-honsed-defmapping-info
- Constructor macro for honsed defmapping-infop structures.
- Defmapping-info->unconditional
- Access the unconditional field of a defmapping-infop structure.
- Defmapping-info->expansion
- Access the expansion field of a defmapping-infop structure.
- Defmapping-info->domb-guard
- Access the domb-guard field of a defmapping-infop structure.
- Defmapping-info->domb
- Access the domb field of a defmapping-infop structure.
- Defmapping-info->doma-guard
- Access the doma-guard field of a defmapping-infop structure.
- Defmapping-info->doma
- Access the doma field of a defmapping-infop structure.
- Defmapping-info->call$
- Access the call$ field of a defmapping-infop structure.
- Defmapping-info->beta-of-alpha
- Access the beta-of-alpha field of a defmapping-infop structure.
- Defmapping-info->beta-injective
- Access the beta-injective field of a defmapping-infop structure.
- Defmapping-info->beta-image
- Access the beta-image field of a defmapping-infop structure.
- Defmapping-info->beta-guard
- Access the beta-guard field of a defmapping-infop structure.
- Defmapping-info->beta
- Access the beta field of a defmapping-infop structure.
- Defmapping-info->alpha-of-beta
- Access the alpha-of-beta field of a defmapping-infop structure.
- Defmapping-info->alpha-injective
- Access the alpha-injective field of a defmapping-infop structure.
- Defmapping-info->alpha-image
- Access the alpha-image field of a defmapping-infop structure.
- Defmapping-info->alpha-guard
- Access the alpha-guard field of a defmapping-infop structure.
- Defmapping-info->alpha
- Access the alpha field of a defmapping-infop structure.
