Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC