Documentation

Mathlib.Tactic.Hint

The hint tactic. #

The hint tactic tries the kitchen sink: it runs every tactic registered via the register_hint 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 (Lean.TSyntax `tactic) (List (Lean.TSyntax `tactic))

An environment extension for registering hint tactics.

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

Register a new hint tactic.

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

Return the list of registered hint tactics.

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

Register a tactic for use with the hint tactic, e.g. register_hint simp_all.

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Hint.suggestion (tac : Lean.TSyntax `tactic) (msgs : Lean.MessageLog := { hadErrors := false, unreported := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, reportedKinds := ∅ }) :
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.
source
def Mathlib.Tactic.Hint.withMessageLog (t : Lean.Elab.Tactic.TacticM Unit) :
Lean.Elab.Tactic.TacticM Lean.MessageLog

Run a tactic, returning any new messages rather than adding them to the message log.

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Hint.withoutInfoTrees (t : Lean.Elab.Tactic.TacticM Unit) :
Lean.Elab.Tactic.TacticM Unit

Run a tactic, but revert any changes to info trees. We use this to inhibit the creation of widgets by subsidiary tactics.

Equations
  • One or more equations did not get rendered due to their size.
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.
source
def Mathlib.Tactic.Hint.hintStx :
Lean.ParserDescr

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

Equations