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]

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

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

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.

Equations

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

def Mathlib.Tactic.Says.evalTacticCapturingMessages (tac : Lean.TSyntax `tactic) (only : optParam (Lean.Message → Bool) fun x => 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

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

def Mathlib.Tactic.Says.evalTacticCapturingInfo (tac : Lean.TSyntax `tactic) : Lean.Elab.Tactic.TacticM (List Lean.Message)

Run evalTactic, capturing any new info messages.

Equations

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

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.

def Mathlib.Tactic.Says.says : Lean.TrailingParserDescr

Equations

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