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

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

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

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

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

source
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`.

Equations

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

Instances For

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

Instances For

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

Equations

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

Instances For