# 'Try this' tactic macro #

This is a convenient shorthand intended for macro authors to be able to generate "Try this" recommendations. (It is not the main implementation of 'Try this', which is implemented in Lean core, see `Lean.Meta.Tactic.TryThis`.)

source
def Mathlib.Tactic.tacticTry_this__ :
Lean.ParserDescr

Produces the text `Try this: <tac>` with the given tactic, and then executes it.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.convTry_this__ :
Lean.ParserDescr

Produces the text `Try this: <tac>` with the given conv tactic, and then executes it.

Equations

- One or more equations did not get rendered due to their size.

Instances For