Zulip Chat Archive

Stream: general

Topic: Docs show overly simplistic theorem statement


view this post on Zulip Eric Wieser (Sep 27 2020 at 11:55):

Just looked at docs#module_ext - the version visible in the docs has the same LHS and RHS, since the instance annotations are missing.

view this post on Zulip Bryan Gin-ge Chen (Sep 27 2020 at 15:46):

Please open an issue for this in the doc-gen repo. Github is generally a better place to track bugs like this than Zulip.

view this post on Zulip Eric Wieser (Sep 27 2020 at 16:49):

https://github.com/leanprover-community/doc-gen/issues/78


Last updated: May 17 2021 at 21:12 UTC