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