incompleteness in doc

Stream: new members

[Chris M]

It seems like the wlog tactic in the mathlib doc has an incomplete description. It says: Given a goal of the form g xs, a predicate p over a set of variables, as well as variable permutations xs_i. Then wlog produces goals of the form, but then doesn't describe the goal.

[Scott Morrison]

Sounds like a good PR! :-)

[Chris M]

Ok, I'll do the PR, except I'm not sure what to add. Here is the link to the docs btw: https://leanprover-community.github.io/mathlib_docs/tactics.html#wlog

[Jalex Stark]

you can also write tactic#wlog and zulip will generate the link for you

[Chris M]

oh, thanks