namespaces should be able to have doc comments

Stream: lean4

[Alok Singh]

i don't know how this would interact with multiple namespace sections which are rather common, but this picture of a python module with documentation inspired me to want something more than the current setup. I want to hover over an import and get a bit of docstring.

2025-04-07-18-25-36.png

[Henrik Böving]

Imports and namespace are completely disjoint concepts, are you asking for hover on imports or hover on namespaces here?

[Alok Singh]

thinking about it, on imports. maybe all the module comments concatenated together could be the import's doc.

[Eric Wieser]

I think just the first one would be fine

[Asei Inoue]

I want this (import documentation) too

[Jovan Gerbscheid]

Since mathlib already enforces us to write module headers, why not display them on hover? :smiley: