如何在 vsc 上的 agda 中转到模块的定义
在 Visual Studio 代码中，转到定义不适用于 agda 模块。我检查了 agda-mode 的键绑定，唯一有用的似乎是 cc co，但这似乎没有找到一些已加载的模块并给出
Panic: Unbound name:
Relation.Binary.PropositionalEquality.Core.erefl[0,2,4,6,30]@ModuleNameHash
6189151057044369179
when retrieving the contents of a module
错误消息。在许多情况下，找到一个函数的定义而不是整个模块会很有帮助。
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.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
鼠标中键（适用于 Emacs）对我来说也不起作用。但是，您可以右键单击并选择“转到定义”，或者只需按 F12，它应该会将您带到定义，因为您已经使用 Cc Cl 加载了文件。
The middle mouse shortcut (which works on Emacs) did not work for me either. However, you can just rightclick and select "go to definition" or just press F12 and it should bring you to the definition, given you have loaded the file with C-c C-l.