mathlib3 documentation

tactic.hint

source
meta def tactic.hint.hint_tactic_attribute  :
(user_attribute unit)

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

source
def tactic_doc.attribute.hint_tactic  :
tactic_doc_entry

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

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

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
def tactic_doc.command.add_hint_tactic  :
tactic_doc_entry

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.

source
def tactic_doc.tactic.hint  :
tactic_doc_entry

hint lists possible tactics which will make progress (that is, not fail) against the current goal.

example {P Q : Prop} (p : P) (h : P → Q) : Q :=
begin
  hint,
  /- the following tactics make progress:
     ----
     Try this: solve_by_elim
     Try this: finish
     Try this: tauto
  -/
  solve_by_elim,
end

You can add a tactic to the list that hint tries by either using

  1. attribute [hint_tactic] my_tactic, if my_tactic is already of type tactic string (tactic unit is allowed too, in which case the printed string will be the name of the tactic), or
  2. add_hint_tactic "my_tactic", specifying a string which works as an interactive tactic.