public class NoFindTacletBuilder extends TacletBuilder<NoFindTaclet>
Taclet
s, they are created in the parsers
using TacletBuilder
s. This builder is used for
NoFindTaclet
rules. Besides this some tests are performed that avoid
some common errors on applicability of taclets.TacletBuilder.TacletBuilderException
attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn
Constructor and Description |
---|
NoFindTacletBuilder() |
Modifier and Type | Method and Description |
---|---|
void |
addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
protected void |
checkBoundInIfAndFind()
checks that a variableSV occurrs at most once in a quantifier of the
ifs and finds and throws an exception otherwise
|
NoFindTaclet |
getNoFindTaclet()
builds and returns the RewriteTaclet that is specified by
former set... / add... methods.
|
NoFindTaclet |
getTaclet()
builds and returns the Taclet that is specified by
former set... / add... methods.
|
addGoal2ChoicesMapping, addRuleSet, addVariableCondition, addVarsNew, addVarsNew, addVarsNew, addVarsNew, addVarsNewDependingOn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, checkContainsFreeVarSV, checkContainsFreeVarSV, getChoices, getGoal2Choices, getName, getTacletWithoutInactiveGoalTemplates, goalTemplates, ifSequent, setAnnotations, setChoices, setDisplayName, setHelpText, setIfSequent, setName, setRuleSets, setTacletGoalTemplates, setTrigger, varsNotFreeIn
public NoFindTaclet getNoFindTaclet()
public void addTacletGoalTemplate(TacletGoalTemplate goal)
addTacletGoalTemplate
in class TacletBuilder<NoFindTaclet>
goal
- the TacletGoalTemplate specifying all the changes to be made
to achieve one of the resulting goalsprotected void checkBoundInIfAndFind()
public NoFindTaclet getTaclet()
getTaclet
in class TacletBuilder<NoFindTaclet>