public class NoFindTacletExecutor extends TacletExecutor<NoFindTaclet>
taclet
Constructor and Description |
---|
NoFindTacletExecutor(NoFindTaclet taclet) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
protected void |
applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace
public NoFindTacletExecutor(NoFindTaclet taclet)
protected void applyAdd(TermLabelState termLabelState, Sequent add, SequentChangeInfo currentSequent, Services services, MatchConditions matchCond, Goal goal, RuleApp ruleApp)
termLabelState
- The TermLabelState
of the current rule application.add
- the Sequent to be addedcurrentSequent
- the Sequent which is the current (intermediate) result of
applying the tacletservices
- the Services encapsulating all java informationmatchCond
- the MatchConditions with all required instantiationspublic ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
apply
in interface RuleExecutor
apply
in class TacletExecutor<NoFindTaclet>
goal
- the goal that the rule application should refer to.services
- the Services encapsulating all java informationruleApp
- the taclet application that is executed