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.parseAsTacticSeq (env : Lean.Environment) (input : String) (fileName : String := "<input>") : Except String (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

This is a slight modification of Parser.runParserCategory.

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.

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

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