public class SuccTaclet extends FindTaclet
Taclet.TacletLabelHint
Modifier and Type | Field and Description |
---|---|
private boolean |
ignoreTopLevelUpdates |
find
choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString
Constructor and Description |
---|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Modifier and Type | Method and Description |
---|---|
protected void |
createAndInitializeExecutor() |
boolean |
ignoreTopLevelUpdates()
this method is used to determine if top level updates are
allowed to be ignored.
|
SuccTaclet |
setName(java.lang.String s) |
protected java.lang.StringBuffer |
toStringFind(java.lang.StringBuffer sb)
toString for the find part
|
equals, find, getBoundVariablesHelper, getIfFindVariables, hashCode, toString
admissible, admissibleAutomatic, admissibleInteractive, apply, closeGoal, collectSchemaVars, createAndInitializeMatcher, createTacletServices, displayName, getBoundVariables, getChoices, getExecutor, getIfVariables, getMatcher, getNameCorrespondent, getPrefix, getRuleJustification, getRuleSets, getSurviveSymbExec, getTrigger, getVariableConditions, goalTemplates, hasReplaceWith, hasTrigger, ifSequent, isContextInPrefix, name, prefixMap, ruleSets, toStringAttribs, toStringGoalTemplates, toStringIf, toStringRuleSets, toStringVarCond, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn
public SuccTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> heuristics, TacletAttributes attrs, Term find, boolean ignoreTopLevelUpdates, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations)
name
- the name of the TacletapplPart
- contains the application part of an Taclet that is
the if-sequent, the variable conditionsgoalTemplates
- a list of goal descriptions.heuristics
- a list of heurisics for the Tacletattrs
- attributes for the Taclet; these are boolean values
indicating a noninteractive or recursive use of the Taclet.find
- the find term of the TacletprefixMap
- a ImmMapprotected void createAndInitializeExecutor()
createAndInitializeExecutor
in class Taclet
public boolean ignoreTopLevelUpdates()
ignoreTopLevelUpdates
in class FindTaclet
protected java.lang.StringBuffer toStringFind(java.lang.StringBuffer sb)
toStringFind
in class FindTaclet
public SuccTaclet setName(java.lang.String s)