public abstract class FindTacletBuilder<T extends FindTaclet> extends TacletBuilder<T>
TacletBuilder.TacletBuilderException
Modifier and Type | Field and Description |
---|---|
protected Term |
find |
attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn
Constructor and Description |
---|
FindTacletBuilder() |
Modifier and Type | Method and Description |
---|---|
protected void |
checkBoundInIfAndFind()
checks that a SchemaVariable that is used to match pure variables
(this means bound variables) occurs at most once in a quantifier of the
assumes and finds and throws an exception otherwise
|
Term |
getFind() |
addGoal2ChoicesMapping, addRuleSet, addTacletGoalTemplate, addVariableCondition, addVarsNew, addVarsNew, addVarsNew, addVarsNew, addVarsNewDependingOn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, checkContainsFreeVarSV, checkContainsFreeVarSV, getChoices, getGoal2Choices, getName, getTaclet, getTacletWithoutInactiveGoalTemplates, goalTemplates, ifSequent, setAnnotations, setChoices, setDisplayName, setHelpText, setIfSequent, setName, setRuleSets, setTacletGoalTemplates, setTrigger, varsNotFreeIn
protected Term find
protected void checkBoundInIfAndFind()
public Term getFind()