Package | Description |
---|---|
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.tacletbuilder |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printNewVarcond(NewVarcond sv) |
Modifier and Type | Method and Description |
---|---|
NewVarcond |
Taclet.varDeclaredNew(SchemaVariable var)
looks if a variable is declared as new and returns its sort to match
with or the schema variable it shares the match-sort with.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<NewVarcond> |
Taclet.varsNew()
returns an iterator over the variables that are new in the Taclet.
|
ImmutableList<NewVarcond> |
TacletApplPart.varsNew()
returns the list of variables that are new in a Taclet
|
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 | Field and Description |
---|---|
protected ImmutableList<NewVarcond> |
TacletBuilder.varsNew |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNew(NewVarcond nv)
adds a new new variable to the variable conditions of
the Taclet: v is new.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNew(ImmutableList<NewVarcond> list)
adds a list of new variables to the variable conditions of
the Taclet: v is new for all v's in the given list
|
Copyright © 2003-2019 The KeY-Project.