## Stream: new members

### Topic: incompleteness in doc

#### Chris M (Jul 25 2020 at 04:13):

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 (Jul 25 2020 at 04:15):

Sounds like a good PR! :-)

#### Chris M (Jul 25 2020 at 04:27):

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 (Jul 25 2020 at 04:28):

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

#### Chris M (Jul 25 2020 at 04:29):

oh, thanks

Last updated: May 09 2021 at 18:17 UTC