## Stream: general

### Topic: doc-gen#54

#### 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

#### 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

#### Mario Carneiro (Aug 26 2020 at 17:42):

Do you have examples with many typeclass arguments?

#### 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