Zulip Chat Archive

Stream: new members

Topic: incompleteness in doc


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 25 2020 at 04:15):

Sounds like a good PR! :-)

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 25 2020 at 04:28):

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

view this post on Zulip Chris M (Jul 25 2020 at 04:29):

oh, thanks


Last updated: May 09 2021 at 18:17 UTC