Zulip Chat Archive

Stream: lean4

Topic: namespaces should be able to have doc comments


Alok Singh (Apr 07 2025 at 22:27):

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 (Apr 07 2025 at 22:29):

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

Alok Singh (Apr 07 2025 at 22:30):

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

Eric Wieser (Apr 07 2025 at 23:01):

I think just the first one would be fine


Last updated: May 02 2025 at 03:31 UTC