Documentation

Mathlib.Tactic.TryThis

'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.)

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

Equations
    Instances For

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

      Equations
        Instances For