# mathlibdocumentation

tactic.hint

An attribute marking a tactic unit or tactic string which should be used by the 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.