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 |