public class TacletApplPart
extends java.lang.Object
Constructor and Description |
---|
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> 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.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<VariableCondition> |
getVariableConditions()
returns the list of additional generic conditions on
instantiations of schema variables.
|
Sequent |
ifSequent()
returns the if-sequent of the application part of a Taclet
|
ImmutableList<NewVarcond> |
varsNew()
returns the list of variables that are new in a Taclet
|
ImmutableList<NewDependingOn> |
varsNewDependingOn()
returns the list of variable pairs that represent the
"new depending on" relation of a Taclet
|
ImmutableList<NotFreeIn> |
varsNotFreeIn()
returns the list of variable pairs that represent the
NotFreeIn relation of a Taclet
|
public TacletApplPart(Sequent ifseq, ImmutableList<NewVarcond> varsNew, ImmutableList<NotFreeIn> varsNotFreeIn, ImmutableList<NewDependingOn> varsNewDependingOn, ImmutableList<VariableCondition> variableConditions)
public Sequent ifSequent()
public ImmutableList<NewVarcond> varsNew()
public ImmutableList<NotFreeIn> varsNotFreeIn()
public ImmutableList<NewDependingOn> varsNewDependingOn()
public ImmutableList<VariableCondition> getVariableConditions()
Copyright © 2003-2019 The KeY-Project.