|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.AbstractMetaOperator
de.uka.ilkd.key.rule.metaconstruct.arith.MetaEqual
| MetaEqual | | public class MetaEqual extends AbstractMetaOperator (Code) | | this class implements the interface for
MetaAdderators. MetaAdderators are used to do complex term
transformation when applying a taclet. Often these transformation
caanot be described with the taclet scheme (or trying to do so would
result in a huge number of rules)
|
| Method Summary | |
| public Term | calculate(Term term, SVInstantiations svInst, Services services)
calculates the resulting term. | | public boolean | validTopLevel(Term term)
checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator. |
| MetaEqual | | public MetaEqual()(Code) | | |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator. The
assumption that the top level operator and the term are equal
is NOT checked.
true iff the top level structure ofthe @link Term is valid. |
|
|
|