public class ConstraintAwareSyntacticalReplaceVisitor extends SyntacticalReplaceVisitor
Modifier and Type | Field and Description |
---|---|
private Constraint |
metavariableInst
Deprecated.
|
applicationPosInOccurrence, goal, labelHint, rule, ruleApp, services, SUBSTITUTION_WITH_LABELS_HINT, svInst, tb, termLabelState
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected Term |
toTerm(Term t)
the method is only still invoked to allow the
ConstraintAwareSyntacticalReplaceVisitor
to recursively replace meta variables |
void |
visited(Term visited) |
getSVInstantiations, getTerm, pushNew, subtreeEntered, subtreeLeft, visit
visitSubtree
@Deprecated private final Constraint metavariableInst
public ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState, Services services, Constraint metavariableInst, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Taclet.TacletLabelHint labelHint, Goal goal)
protected Term toTerm(Term t)
SyntacticalReplaceVisitor
ConstraintAwareSyntacticalReplaceVisitor
to recursively replace meta variablestoTerm
in class SyntacticalReplaceVisitor
public void visited(Term visited)