de.uka.ilkd.key.rule.inst

Class OperatorInstantiation

java.lang.Object

de.uka.ilkd.key.rule.inst.InstantiationEntry<Operator>

de.uka.ilkd.key.rule.inst.OperatorInstantiation

public class OperatorInstantiation
extends InstantiationEntry<Operator>

This class is used to store the instantiation of a schemavarible if it is an operator.

Constructor Summary

Constructors

Constructor and Description
OperatorInstantiation(Operator op) creates a new ContextInstantiationEntry

Method Summary

Methods inherited from class de.uka.ilkd.key.rule.inst.InstantiationEntry

equals, getInstantiation, hashCode, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

OperatorInstantiation

OperatorInstantiation(Operator op)

creates a new ContextInstantiationEntry

Parameters:

op - the Operator the SchemaVariable is instantiated with