public interface RuleCompletionHandler
AbstractProofControl
to complete a Rule
completion.Modifier and Type | Method and Description |
---|---|
void |
completeAndApplyTacletMatch(TacletInstantiationModel[] models,
Goal goal)
called to complete and apply a taclet instantiations
|
IBuiltInRuleApp |
completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced)
completes rule applications of built in rules
|
void completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal goal)
models
- the partial models with all different possible instantiations found automaticallygoal
- the Goal where to applyIBuiltInRuleApp completeBuiltInRuleApp(IBuiltInRuleApp app, Goal goal, boolean forced)
app
- the DefaultBuiltInRuleApp to be completedgoal
- the Goal where the app will later be applied toforced
- a boolean indicating if the rule should be applied without any
additional interaction from the user provided that the application object can be
made complete automatically