In some VSCode extensions one can press control to get extra info in the popup already shown when one hovers a symbol.
In MathComp we have a command HB.about (akin to About) which prints extra info very relevant to the context of this library.
We would like to have this info printed somehow.
Some naive questions:
is the "show more" an additional query to the language server?
would it make sense to piggy back on About making it extensible on the Coq side (eg in MathComp when you call About you also call HB.about)?
In some VSCode extensions one can press control to get extra info in the popup already shown when one hovers a symbol. In MathComp we have a command
HB.about
(akin toAbout
) which prints extra info very relevant to the context of this library.We would like to have this info printed somehow.
Some naive questions:
About
making it extensible on the Coq side (eg in MathComp when you callAbout
you also callHB.about
)?