public class AntecSuccTacletGoalTemplate extends TacletGoalTemplate
Modifier and Type | Field and Description |
---|---|
private Sequent |
replacewith
sequent that replaces another one
|
Constructor and Description |
---|
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith) |
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object o) |
ImmutableSet<QuantifiableVariable> |
getBoundVariables()
rertieves and returns all variables that are bound in the
goal template
|
int |
hashCode() |
Sequent |
replaceWith()
a Taclet may replace a Sequent by another.
|
java.lang.Object |
replaceWithExpressionAsObject()
a Taclet may replace parts of sequent.
|
java.lang.String |
toString()
toString
|
addedProgVars, name, rules, sequent, setName
private Sequent replacewith
public AntecSuccTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Sequent replacewith, ImmutableSet<SchemaVariable> pvs)
addedSeq
- new Sequent to be addedaddedRules
- IListreplacewith
- the Sequent that replaces another onepublic AntecSuccTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Sequent replacewith)
public Sequent replaceWith()
public ImmutableSet<QuantifiableVariable> getBoundVariables()
getBoundVariables
in class TacletGoalTemplate
public java.lang.Object replaceWithExpressionAsObject()
TacletGoalTemplate
replaceWithExpressionAsObject
in class TacletGoalTemplate
public boolean equals(java.lang.Object o)
equals
in class TacletGoalTemplate
public int hashCode()
hashCode
in class TacletGoalTemplate
public java.lang.String toString()
toString
in class TacletGoalTemplate