# The `hint` tactic. #

The `hint` tactic tries the kitchen sink: it runs every tactic registered via the `register_hint <prio> tac` command on the current goal, and reports which ones succeed.

## Future work #

It would be nice to run the tactics in parallel.

source
opaque Mathlib.Tactic.Hint.hintExtension :
Lean.SimplePersistentEnvExtension (Nat × Lean.TSyntax `tactic) (List (Nat × Lean.TSyntax `tactic))

An environment extension for registering hint tactics with priorities.

source
def Mathlib.Tactic.Hint.addHint (prio : Nat) (stx : Lean.TSyntax `tactic) :
Lean.CoreM Unit

Register a new hint tactic.

Equations

- Mathlib.Tactic.Hint.addHint prio stx = Lean.modifyEnv fun (env : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Mathlib.Tactic.Hint.hintExtension env (prio, stx)

Instances For

source
def Mathlib.Tactic.Hint.getHints :
Lean.CoreM (List (Nat × Lean.TSyntax `tactic))

Return the list of registered hint tactics.

Equations

- Mathlib.Tactic.Hint.getHints = do let __do_lift ← Lean.getEnv pure (Mathlib.Tactic.Hint.hintExtension.getState __do_lift)

Instances For

source
def Mathlib.Tactic.Hint.registerHintStx :
Lean.ParserDescr

Register a tactic for use with the `hint` tactic, e.g. `register_hint 1000 simp_all`. The numeric argument specifies the priority: tactics with larger priorities run before those with smaller priorities. The priority must be provided explicitly.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Hint.suggestion (tac : Lean.TSyntax `tactic) (trees : Lean.PersistentArray Lean.Elab.InfoTree) :
Lean.Elab.Tactic.TacticM Lean.Meta.Tactic.TryThis.Suggestion

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

source
def Mathlib.Tactic.Hint.hint (stx : Lean.Syntax) :
Lean.Elab.Tactic.TacticM Unit

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

source
def Mathlib.Tactic.Hint.hintStx :
Lean.ParserDescr

The `hint` tactic tries every tactic registered using `register_hint <prio> tac`, and reports any that succeed.

Equations

- Mathlib.Tactic.Hint.hintStx = Lean.ParserDescr.node `Mathlib.Tactic.Hint.hintStx 1024 (Lean.ParserDescr.nonReservedSymbol "hint" false)

Instances For