Lake.Name instead of Lean.Name?

Stream: lean4

[Damiano Testa]

Looking at docs#Lean.Name the constructors for me mention Lake.Name, instead of what I thought should be Lean.Name.

Does anyone else see the same? Should they be indeed Lean.Name instead?

This seems to happen every time Lean.Name appears anywhere other than in the declaration name.

[Damiano Testa]

This is what I see (underlining to highlight the Lake/Lean issue):

1059c817-6337-48cb-ab03-10a7ca414619.jpg

[Jireh Loreaux]

This is a known issue, yes.

[Jireh Loreaux]

I can't remember whether it is a lake or docgen issue, but there's another thread lurking about it somewhere.

[Utensil Song]

See https://github.com/leanprover/lean4/issues/2524 and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Confusing.20delaboration.20in.20.20doc-gen/near/388165262

[Damiano Testa]

Great, thanks! I had missed those discussions.