In visual studio code, the go to definition doesn't work for agda modules. I checked the key-bindings for agda-mode and the only one useful seemed c-c c-o but that doesn't seem to find some loaded modules and gives
Panic: Unbound name:
Relation.Binary.PropositionalEquality.Core.erefl[0,2,4,6,30]@ModuleNameHash
6189151057044369179
when retrieving the contents of a module
error message. And in many instances it would be helpful to find a definition for just a function instead of the whole module.