doc-gen#54

Stream: general

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Mario Carneiro]

Do you have examples with many typeclass arguments?

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

Just to say that I'm loving this feature.