public class RewriteTacletGoalTemplate extends TacletGoalTemplate
AntecSuccTacletGoalTemplate
Modifier and Type | Field and Description |
---|---|
private Term |
replacewith
term that replaces another one
|
Constructor and Description |
---|
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith) |
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
RewriteTacletGoalTemplate(Term replacewith) |
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() |
Term |
replaceWith()
a Taclet may replace a Term by another.
|
java.lang.Object |
replaceWithExpressionAsObject()
a Taclet may replace parts of sequent.
|
java.lang.String |
toString()
toString
|
addedProgVars, name, rules, sequent, setName
private Term replacewith
public RewriteTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Term replacewith, ImmutableSet<SchemaVariable> pvs)
addedSeq
- new Sequent to be addedaddedRules
- IListreplacewith
- the Term that replaces another onepvs
- the set of schema variablespublic RewriteTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Term replacewith)
public RewriteTacletGoalTemplate(Term replacewith)
public Term 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