de.uka.ilkd.key.rule.match.vm.instructions

Class BindVariablesInstruction

java.lang.Object

de.uka.ilkd.key.rule.match.vm.instructions.BindVariablesInstruction

All Implemented Interfaces:

MatchInstruction

public class BindVariablesInstruction
extends java.lang.Object
implements MatchInstruction

This instructions matches the variable below a binder (e.g. a quantifier).

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	BindVariablesInstruction.LogicVariableBinder
private static interface	BindVariablesInstruction.VariableBinderSubinstruction
private static class	BindVariablesInstruction.VariableSVBinder

Field Summary

Fields

Modifier and Type	Field and Description
private BindVariablesInstruction.VariableBinderSubinstruction[]	boundVarBinders

Constructor Summary

Constructors

Constructor and Description
BindVariablesInstruction(ImmutableArray<QuantifiableVariable> boundVars)

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(TermNavigator termPosition, MatchConditions matchConditions, Services services)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

boundVarBinders

private final BindVariablesInstruction.VariableBinderSubinstruction[] boundVarBinders

Constructor Detail

BindVariablesInstruction

public BindVariablesInstruction(ImmutableArray<QuantifiableVariable> boundVars)

Method Detail

match

public MatchConditions match(TermNavigator termPosition,
                             MatchConditions matchConditions,
                             Services services)

Specified by:

match in interface MatchInstruction