Wiki page for tactic combinators?

Stream: mathlib4

[Thomas Murrills]

Is there a place where all of the tactic combinators and "control flow"-esque tactics ({}, try, first, ;, <;>, all_goals, etc.) are listed already? If not, would it be helpful to have a wiki page on mathlib4 for them?

[Kyle Miller]

For conv mode, I made such a page of combinators (and tactics) here: https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html

Maybe there could be another guide for tactic combinators?

[Thomas Murrills]

Nice! Maybe I'll start it. :) By the way, do we have a rule of thumb for when something should be in mathlib4/docs and when it should be a wiki page on the repo?