Zulip Chat Archive

Stream: general

Topic: doc-gen#54


view this post on Zulip Gabriel Ebner (Aug 26 2020 at 17:35):

There is a proposed change to the mathlib documentation that changes the way implicit arguments are (not) printed. Right now, they are by default collapsed to {…} and are expanded once you figure out that you can click on it. After doc-gen#54, the implicit arguments would instead be grayed-out (they return to normal if you hover over them). Thoughts?
gray_out_example.png

view this post on Zulip Gabriel Ebner (Aug 26 2020 at 17:35):

You can try it out here: https://gebner.github.io/mathlib_docs/algebra/group_with_zero.html#mul_ne_zero_iff

view this post on Zulip Mario Carneiro (Aug 26 2020 at 17:42):

Do you have examples with many typeclass arguments?

view this post on Zulip Bryan Gin-ge Chen (Aug 26 2020 at 17:44):

Here's one example: https://gebner.github.io/mathlib_docs/geometry/manifold/basic_smooth_bundle.html#basic_smooth_bundle_core

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 17:03):

Just to say that I'm loving this feature.


Last updated: May 08 2021 at 02:46 UTC