|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.SubstOp
All known Subclasses: de.uka.ilkd.key.logic.op.WarySubstOp,
| SubstOp | | public class SubstOp extends Op (Code) | | Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators. Currently, only the subclass WarySubstOp is used
and accessible through the key parser.
|
| apply | | public Term apply(Term term)(Code) | | Apply this substitution operator to term, which
has this operator as top-level operator
|
| arity | | public int arity()(Code) | | arity of the Substitution operator as int |
| sort | | public Sort sort(Term[] term)(Code) | | sort of the second subterm or throws anIllegalArgumentException if the given term has no correct (2=) arity |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | true iff the sort of the subterm 0 of the given termhas the same sort as or a subsort of the variable to be substituted and theterm's arity is 2 and the numer of variables bound there is 0for the 0th subterm and 1 for the 1st subterm. |
|
|
|