Documentation for Array.mk/List.toArray

Stream: lean4

[Johannes Tantow]

Hi,
the documentation of List.toArrayhere https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Array.mk is a bit confusing as it apparently refers to itself. Looking into the source code I see that the documentation is inherited from Array.mk, which explains the text. The documentation for Array.mk is however not displayed. Is this intended?

[Kim Morrison]

@Johannes Tantow, thanks for the report, fixed on lean#6962

[Johannes Tantow]

Thanks. What about the other part, i.e. that the text for the constructor and the constructor itself is not displayed? Or is that a mathlib-website problem?

[Kim Morrison]

I think this will be fixed on the next release.