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.
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