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.

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

An environment extension for registering hint tactics with priorities.

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

Register a new hint tactic.

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

Return the list of registered hint tactics.

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.

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.

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.

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

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