public class TacletGoalTemplate
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<SchemaVariable> |
addedProgVars
program variables added by this taclet to the namespace
|
private ImmutableList<Taclet> |
addedRules
stores list of Taclet which are introduced
|
private Sequent |
addedSeq
stores sequent that is one of the new goals
|
private java.lang.String |
name |
Constructor and Description |
---|
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules)
creates new Goaldescription
same effect as
new TacletGoalTemplate(addedSeq,
addedRules,
SetAsListOf. |
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
ImmutableSet<SchemaVariable> addedProgVars)
creates new Goaldescription
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<SchemaVariable> |
addedProgVars()
returns the set of schemavaroable whose instantiations will be
added to the sequent namespace
|
boolean |
equals(java.lang.Object o) |
ImmutableSet<QuantifiableVariable> |
getBoundVariables()
retrieves and returns all variables that are bound in the
goal template
|
int |
hashCode() |
java.lang.String |
name() |
java.lang.Object |
replaceWithExpressionAsObject()
a Taclet may replace parts of sequent.
|
ImmutableList<Taclet> |
rules()
the goal of a Taclet may introduce new rules.
|
Sequent |
sequent()
a Taclet may add a new Sequent as Goal.
|
void |
setName(java.lang.String s) |
java.lang.String |
toString() |
private Sequent addedSeq
private ImmutableList<Taclet> addedRules
private ImmutableSet<SchemaVariable> addedProgVars
private java.lang.String name
public TacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, ImmutableSet<SchemaVariable> addedProgVars)
addedSeq
- new Sequent to be addedaddedRules
- IListaddedProgVars
- a SetOfpublic TacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules)
new TacletGoalTemplate(addedSeq,
addedRules,
SetAsListOf.nil())
addedSeq
- new Sequent to be addedaddedRules
- IListpublic java.lang.Object replaceWithExpressionAsObject()
public Sequent sequent()
public ImmutableList<Taclet> rules()
public ImmutableSet<SchemaVariable> addedProgVars()
public ImmutableSet<QuantifiableVariable> getBoundVariables()
public void setName(java.lang.String s)
public java.lang.String name()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object