de.uka.ilkd.key.rule.inst

Class TermInstantiation

java.lang.Object

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

de.uka.ilkd.key.rule.inst.TermInstantiation

public class TermInstantiation
extends InstantiationEntry<Term>

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

Field Summary

Fields

Modifier and Type	Field and Description
private static RigidnessException	RIGIDNESS_EXCEPTION

Constructor Summary

Constructors

Constructor and Description
TermInstantiation(SchemaVariable sv, Term term) 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

Field Detail

RIGIDNESS_EXCEPTION

private static final RigidnessException RIGIDNESS_EXCEPTION

Constructor Detail

TermInstantiation

TermInstantiation(SchemaVariable sv,
                  Term term)

creates a new ContextInstantiationEntry

Parameters:

sv - the SchemaVariable that is instantiated

term - the Term the SchemaVariable is instantiated with