| Interface | Description |
|---|---|
| ProjectionToTerm |
Interface for mappings from rule applications to terms.
|
| Class | Description |
|---|---|
| AbstractDividePolynomialsProjection | |
| AssumptionProjection |
Term projection that delivers the assumptions of a taclet application
(the formulas that the \assumes clause of the taclet refers to).
|
| CoeffGcdProjection |
Given a monomial and a polynomial, this projection computes the gcd of all
numerical coefficients.
|
| DividePolynomialsProjection | |
| FocusFormulaProjection | |
| FocusProjection |
Projection of a rule application to its focus (the term or formula that the
rule operates on, that for taclets is described using
\find,
and that can be modified by the rule). |
| MonomialColumnOp | |
| ReduceMonomialsProjection |
Projection for dividing one monomial by another.
|
| SubtermProjection |
Projection for computing a subterm of a given term.
|
| SVInstantiationProjection |
Projection of taclet apps to the instantiation of a schema variable.
|
| TermBuffer |
Projection that can store and returns an arbitrary term or formula.
|
| TermConstructionProjection |
Term projection for constructing a bigger term from a sequence of direct
subterms and an operator.
|
| TriggerVariableInstantiationProjection |