Documentation

Mathlib.Tactic.Says

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

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

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.

Equations
    Instances For

      Run evalTactic, capturing any new messages. The optional only argument allows selecting which messages should be captured, or left in the message log.

      Equations
        Instances For

          Run evalTactic, capturing any new info messages.

          Equations
            Instances For

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

              Equations
                Instances For

                  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
                    Instances For