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

source

opaque Mathlib.Tactic.Says.says.no_verify_in_CI :

Lean.Option Bool

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