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

This is a slight modification of Parser.runParserCategory.

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.

    Instances For

      Run evalTactic, capturing any new info messages.

      Instances For

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

        Instances For