In other languages (at least in Rust), it is possible to associate a "doc comment" with a function, and when hovering a place in the code where that function is called, the doc comment will be shown. That is extremely useful to be able to quickly navigate foreign code.
It would be really nice if vscoq did something similar. I notice that hovering will show basically what About shows, which is already really nice. And probably doing any more is blocked on Coq having such a notion of a "doc comment" in the first place. But I think that would be valuable to have (also e.g. for search), so vscoq could be a motivation for Coq to adopt a system like that. :)
In other languages (at least in Rust), it is possible to associate a "doc comment" with a function, and when hovering a place in the code where that function is called, the doc comment will be shown. That is extremely useful to be able to quickly navigate foreign code.
It would be really nice if vscoq did something similar. I notice that hovering will show basically what
Aboutshows, which is already really nice. And probably doing any more is blocked on Coq having such a notion of a "doc comment" in the first place. But I think that would be valuable to have (also e.g. for search), so vscoq could be a motivation for Coq to adopt a system like that. :)