Modifier and Type | Class and Description |
---|---|
static class |
Taclet.TacletLabelHint.TacletOperation
Defines the possible operations a
Taclet performs. |
Modifier and Type | Field and Description |
---|---|
private Sequent |
sequent
The optional
Sequent of the add or replace part of the taclet. |
private SequentFormula |
sequentFormula
The optional
SequentFormula contained in getSequent() . |
private Taclet.TacletLabelHint.TacletOperation |
tacletOperation
The currently performed operation.
|
private java.util.Deque<Term> |
tacletTermStack
The stack maintained during application of a taclet
Term . |
private Term |
term
The optional replace
Term of the taclet. |
Constructor and Description |
---|
TacletLabelHint(Taclet.TacletLabelHint.TacletOperation tacletOperation,
Sequent sequent)
Constructor.
|
TacletLabelHint(Taclet.TacletLabelHint labelHint,
SequentFormula sequentFormula)
Constructor.
|
TacletLabelHint(Term term)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Sequent |
getSequent()
Returns the optional
Sequent of the add or replace part of the taclet. |
SequentFormula |
getSequentFormula()
Returns the optional
SequentFormula contained in getSequent() . |
Taclet.TacletLabelHint.TacletOperation |
getTacletOperation()
Returns the currently performed operation.
|
java.util.Deque<Term> |
getTacletTermStack()
Returns the stack maintained during application of a taclet
Term . |
Term |
getTerm()
Returns the optional replace
Term of the taclet. |
void |
setTacletTermStack(java.util.Deque<Term> tacletTermStack)
Sets the stack maintained during application of a taclet
Term . |
java.lang.String |
toString() |
private final Taclet.TacletLabelHint.TacletOperation tacletOperation
private final Sequent sequent
Sequent
of the add or replace part of the taclet.private final SequentFormula sequentFormula
SequentFormula
contained in getSequent()
.public TacletLabelHint(Taclet.TacletLabelHint.TacletOperation tacletOperation, Sequent sequent)
tacletOperation
- The currently performed operation.sequent
- The optional Sequent
of the add or replace part of the taclet.public TacletLabelHint(Term term)
tacletOperation
- The currently performed operation.term
- The optional replace Term
of the taclet.public TacletLabelHint(Taclet.TacletLabelHint labelHint, SequentFormula sequentFormula)
labelHint
- The previous Taclet.TacletLabelHint
which is now specialised.sequentFormula
- The optional SequentFormula
contained in getSequent()
.public Taclet.TacletLabelHint.TacletOperation getTacletOperation()
public Sequent getSequent()
Sequent
of the add or replace part of the taclet.Sequent
of the add or replace part of the taclet.public SequentFormula getSequentFormula()
SequentFormula
contained in getSequent()
.SequentFormula
contained in getSequent()
.public java.util.Deque<Term> getTacletTermStack()
Term
.Term
.public void setTacletTermStack(java.util.Deque<Term> tacletTermStack)
Term
.tacletTermStack
- The stack maintained during application of a taclet Term
.public Term getTerm()
Term
of the taclet.Term
of the taclet.public java.lang.String toString()
toString
in class java.lang.Object