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

Instances For

source

def Mathlib.Tactic.Says.evalTacticCapturingMessages (tac : Lean.TSyntax `tactic) (only : Lean.Message → Bool := fun (x : Lean.Message) => true) :

Lean.Elab.Tactic.TacticM (List Lean.Message)

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

source

def Mathlib.Tactic.Says.evalTacticCapturingInfo (tac : Lean.TSyntax `tactic) :

Lean.Elab.Tactic.TacticM (List Lean.Message)

Run evalTactic, capturing any new info messages.

Equations

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.