Lift-info
Fixtype of information about lifted PFCSes.
This is a product type introduced by fty::defprod.
Fields
- pred — symbolp
- def — definition
- hyps — true-list
These are stored in the lift-table.
For each lifted PFCS definition, we store:
- The name of the predicate that represents the lifted definition.
- The abstract syntax tree of the definition.
- A list of terms used as hypotheses in generated theorems
Each term in the list says that
looking up a certain PFCS definition by name
yields the expected abstract syntax of the definition;
there is one such term
for the PFCS definition that this information refers to,
and one such term for each PFCS definition
directly or indirectly called by
the PFCS definition that this information refers to.
Subtopics
- Lift-info-fix
- Fixing function for lift-info structures.
- Lift-info-equiv
- Basic equivalence relation for lift-info structures.
- Make-lift-info
- Basic constructor macro for lift-info structures.
- Change-lift-info
- Modifying constructor for lift-info structures.
- Lift-info->pred
- Get the pred field from a lift-info.
- Lift-info->hyps
- Get the hyps field from a lift-info.
- Lift-info->def
- Get the def field from a lift-info.
- Lift-infop
- Recognizer for lift-info structures.
