public class WaryClashFreeSubst extends ClashFreeSubst
ClashFreeSubst.VariableCollectVisitor
s, svars, tb, v
Constructor and Description |
---|
WaryClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
Term |
apply(Term t)
substitute
s for v in t ,
avoiding collisions by replacing bound variables in
t if necessary. |
protected Term |
apply1(Term t)
substitute
s for v in
t , avoiding collisions by replacing bound
variables in t if necessary. |
applyOnSubterm, getSingleArray, getSubstitutedTerm, getVariable, newVarFor, subTermChanges
public WaryClashFreeSubst(QuantifiableVariable v, Term s, TermBuilder tb)
public Term apply(Term t)
s
for v
in t
,
avoiding collisions by replacing bound variables in
t
if necessary.apply
in class ClashFreeSubst
protected Term apply1(Term t)
s
for v
in
t
, avoiding collisions by replacing bound
variables in t
if necessary. It is
assumed, that t
contains a free occurrence of
v
.apply1
in class ClashFreeSubst
Copyright © 2003-2019 The KeY-Project.