mathlib docs: tactic.hint

meta def tactic.hint.hint_tactic_attribute :

An attribute marking a tactic unit or tactic string which should be used by the hint tactic.

meta def tactic.hint.add_hint_tactic (_x : interactive.parse (lean.parser.tk "add_hint_tactic")) :

add_hint_tactic t runs the tactic t whenever hint is invoked. The typical use case is add_hint_tactic "foo" for some interactive tactic foo.

source

meta def tactic.hint :

tactic (list (string × ℕ))

Report a list of tactics that can make progress against the current goal, and for each such tactic, the number of remaining goals afterwards.

source

meta def tactic.interactive.hint :

tactic unit

Report a list of tactics that can make progress against the current goal.