Zulip Chat Archive

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?

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?

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

Kevin Buzzard (Aug 29 2020 at 17:03):

Just to say that I'm loving this feature.

Last updated: Aug 03 2023 at 10:10 UTC