says

Stream: mathlib4

[Johan Commelin]

Currently the says combinator shows the following text in a hover tooltip:

A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the first tactic of the sequence.

Is it easy to change this to something a bit more appropriate?

[Gareth Ma]

Can you give an example usage? I can't seem to find it
But usually the "fix" is to add documentation to the operator, see <;>

/--
`tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
concatenating all goals produced by `tac'`.
-/
macro:1 x:tactic tk:" <;> " y:tactic:2 : tactic => `(tactic|
  focus
    $x:tactic
    -- annotate token with state after executing `x`
    with_annotate_state $tk skip
    all_goals $y:tactic)

So that if you hover over <;> in

example : true ∧ true := by constructor <;> trivial

There is documentation

[Johan Commelin]

I guess we need to add such a docstring somewhere in Mathlib/Tactic/Says.lean

[Scott Morrison]

@Johan Commelin #7818

[Scott Morrison]

Please change the doc-string to whatever you like!

[Johan Commelin]

Thanks!