| de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm
All known Subclasses: de.uka.ilkd.key.strategy.termProjection.AssumptionProjection, de.uka.ilkd.key.strategy.termProjection.TermConstructionProjection, de.uka.ilkd.key.strategy.termProjection.FocusProjection, de.uka.ilkd.key.strategy.termProjection.SVInstantiationProjection, de.uka.ilkd.key.strategy.termProjection.ReduceMonomialsProjection, de.uka.ilkd.key.strategy.termProjection.SubtermProjection, de.uka.ilkd.key.strategy.termProjection.TermBuffer, de.uka.ilkd.key.strategy.termProjection.CoeffGcdProjection, de.uka.ilkd.key.strategy.termProjection.FocusFormulaProjection, de.uka.ilkd.key.strategy.termProjection.AbstractDividePolynomialsProjection,
ProjectionToTerm | public interface ProjectionToTerm (Code) | | Interface for mappings from rule applications to terms. This is used, for
instance, for determining the instantiation of a schema variable. We also
allow projections to be partial, which is signalled by toTerm
returning null
|
|
|