| java.lang.Object
 de.uka.ilkd.key.rule.TacletApplPart
| TacletApplPart | | public class TacletApplPart (Code) | | |
| Constructor Summary | |
| public | TacletApplPart(Sequent ifseq, ListOfNewVarcond varsNew, ListOfNotFreeIn varsNotFreeIn, ListOfNewDependingOn varsNewDependingOn, ListOfVariableCondition variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions. |
| TacletApplPart | | public TacletApplPart(Sequent ifseq, ListOfNewVarcond varsNew, ListOfNotFreeIn varsNotFreeIn, ListOfNewDependingOn varsNewDependingOn, ListOfVariableCondition variableConditions)(Code) | | constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
| getVariableConditions | | public ListOfVariableCondition getVariableConditions()(Code) | | returns the list of additional generic conditions on
instantiations of schema variables. The list ist readonly.
|
| ifSequent | | public Sequent ifSequent()(Code) | | returns the if-sequent of the application part of a Taclet
|
| varsNew | | public ListOfNewVarcond varsNew()(Code) | | returns the list of variables that are new in a Taclet
|
| varsNewDependingOn | | public ListOfNewDependingOn varsNewDependingOn()(Code) | | returns the list of variable pairs that represent the
"new depending on" relation of a Taclet
|
| varsNotFreeIn | | public ListOfNotFreeIn varsNotFreeIn()(Code) | | returns the list of variable pairs that represent the
NotFreeIn relation of a Taclet
|
|
|