public class AntecSuccTacletGoalTemplate extends TacletGoalTemplate
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
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
Copyright © 2003-2019 The KeY-Project.