The hint
tactic. #
The hint
tactic tries the kitchen sink:
it runs every tactic registered via the register_hint tac
command
on the current goal, and reports which ones succeed.
Future work #
It would be nice to run the tactics in parallel.
An environment extension for registering hint tactics.
Register a new hint tactic.
Equations
Instances For
Return the list of registered hint tactics.
Equations
Instances For
Construct a suggestion for a tactic.
- Check the passed
MessageLog
for an info message beginning with "Try this: ". - If found, use that as the suggestion.
- Otherwise use the provided syntax.
- Also, look for remaining goals and pretty print them after the suggestion.
Equations
Instances For
Run a tactic, returning any new messages rather than adding them to the message log.
Equations
Instances For
Run a tactic, but revert any changes to info trees. We use this to inhibit the creation of widgets by subsidiary tactics.
Equations
Instances For
Run all tactics registered using register_hint
.
Print a "Try these:" suggestion for each of the successful tactics.
If one tactic succeeds and closes the goal, we don't look at subsequent tactics.
Equations
Instances For
The hint
tactic tries every tactic registered using register_hint tac
,
and reports any that succeed.