The says tactic combinator.

If you write X says, where X is a tactic that produces a "Try this: Y" message, then you will get a message "Try this: X says Y". Once you've clicked to replace X says with X says Y, afterwards X says Y will only run Y.

The typical usage case is:

simp? [X] says simp only [X, Y, Z]

If you use set_option says.verify true (set automatically during CI) then X says Y runs X and verifies that it still prints "Try this: Y".

opaque Mathlib.Tactic.Says.says.verify : Lean.Option Bool

If this option is true, verify for X says Y that X says outputs Y.

opaque Mathlib.Tactic.Says.says.no_verify_in_CI : Lean.Option Bool

This option is only used in CI to negate says.verify.

def Mathlib.Tactic.Says.evalTacticCapturingTryThis (tac : Lean.TSyntax `tactic) : Lean.Elab.Tactic.TacticM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Run evalTactic, capturing a "Try this:" message and converting it back to syntax.

Equations

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

def Mathlib.Tactic.Says.says : Lean.TrailingParserDescr

tac₁ says tac₂ runs tac₂. In CI it also runs tac₁ and validates that tac₁ produces a "Try this: tac₂" message. Use set_option says.verify true to enable the validation step on your own machine.

The says combinator is intended to be used when tac₁ is meaningful but slow and tac₂ is faster but hard to read: for example, simp? [X] says simp only [X, Y, Z].

To generate or update the correct value of tac₂, write tac₁ says. You will get a message "Try this: tac₁ says tac₂.

Equations

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