Bundled docs

Stream: mathlib4

[Pedro Sánchez Terraf]

I was checking docs#CategoryTheory.Bundled and noticed that the instance type is rendered as c ↑s, but it would be more reasonable to display it as c α, like the sources. Is this a known issue? Or is there a reason why the current way is better?

[Junyan Xu]

Looks like some pretty printing / delaborator bug ... what is even s?

[Kyle Miller]

It seems to be that s is the name of the structure variable when the documentation is being generated? (I didn't check docgen to verify.)

The attribute [coe] α is what causes the arrow notation to be used. That's there because the α projection is the CoeSort instance, and so you'd want s.α to pretty print as ↑s.

[Junyan Xu]

So you think we should open an issue at https://github.com/leanprover/doc-gen4 ?

[Kyle Miller]

I wonder what it should do instead -- use self rather than s?

[Henrik Böving]

https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/StructureInfo.lean#L23

[Winston Yin (尹維晨)]

Kyle Miller said:

I wonder what it should do instead -- use self rather than s?

I’ve had this confusion before. Given that s is pretty commonly used, I second this suggestion. Or colour s in a special way?

[Henrik Böving]

Changed it to be self

[Eric Wieser]

From the same page: why is the ( linked here:

image.png

[Henrik Böving]

Eric Wieser said:

From the same page: why is the ( linked here:

image.png

sorry, what part is linked that you don't think should be?

[Henrik Böving]

Oh now i see it nvm

[Henrik Böving]

That's not intended, probably a bug either in the delaborator or my analysis of the delaborator output.