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
- Mathlib.Tactic.Hint.addHint stx = Lean.modifyEnv fun (env : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Mathlib.Tactic.Hint.hintExtension env stx
Instances For
Return the list of registered hint tactics.
Equations
- Mathlib.Tactic.Hint.getHints = do let __do_lift ← Lean.getEnv pure (Lean.SimplePersistentEnvExtension.getState Mathlib.Tactic.Hint.hintExtension __do_lift)
Instances For
Register a tactic for use with the hint
tactic, e.g. register_hint simp_all
.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Instances For
Run a tactic, returning any new messages rather than adding them to the message log.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Instances For
The hint
tactic tries every tactic registered using register_hint tac
,
and reports any that succeed.
Equations
- Mathlib.Tactic.Hint.hintStx = Lean.ParserDescr.node `Mathlib.Tactic.Hint.hintStx 1024 (Lean.ParserDescr.nonReservedSymbol "hint" false)