|
|
|---|
|
|
|
|---|
Fixtype of information about lifted PFCSes.
This is a product type introduced by fty::defprod.
These are stored in the lift-table. For each lifted PFCS definition, we store the abstract syntax of the definition and 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.