can't find Quot-related docstrings on docs4

Stream: lean4

[Bulhwi Cha]

It'll be great if we can see the docstrings for Quot, Quot.mk, Quot.ind, and Quot.lift at https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html.

[Bulhwi Cha]

See https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L382-L424.

[Bulhwi Cha]

I can't see this topic in the Recent conversations view. Is this a Zulip bug? I accidentally muted the topic.

[Henrik Böving]

So, these built-in Quot thinngs are treated kinda magically within the Lean environment since they are a quotInfo as opposed to the opaqueInfo one would expect. The responsible line is here: https://github.com/leanprover/doc-gen4/blob/5ab6766eb17a118ed490216305de2a7651e9ebf8/DocGen4/Process/DocInfo.lean#L182 someone could probably play a bit of type tetris with what you get out of a quotInfo and implement this as a rather simple PR if they wanted to. Otherwise I'll get to it at some point :tm: https://github.com/leanprover/doc-gen4/issues/127