Lean4
/-- 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".
-/
@[tactic_parser 1000]
public meta def says : Lean.TrailingParserDescr✝ :=
ParserDescr.trailingNode✝ `Mathlib.Tactic.Says.says 1022 0
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " says")
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt) (ParserDescr.const✝ `tacticSeq))))
