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.printNotFreeIn(NotFreeIn sv) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<NotFreeIn> |
Taclet.varsNotFreeIn()
returns an iterator over the variable pairs that indicate that are
new in the Taclet.
|
ImmutableList<NotFreeIn> |
TacletApplPart.varsNotFreeIn()
returns the list of variable pairs that represent the
NotFreeIn relation of 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<NotFreeIn> |
TacletBuilder.varsNotFreeIn |
Modifier and Type | Method and Description |
---|---|
java.util.Iterator<NotFreeIn> |
TacletBuilder.varsNotFreeIn() |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNotFreeIn(ImmutableList<NotFreeIn> list)
adds a list of NotFreeIn variable pairs to the variable
conditions of
the Taclet: v0 is not free in v1 for all entries (v0,v1) in the given list.
|
Copyright © 2003-2019 The KeY-Project.