如何在 vsc 上的 agda 中找到模块的定义

Question

在 Visual Studio 代码中，转到定义不适用于 agda 模块。我检查了 agda 模式的键绑定，唯一有用的似乎是

c-c c-o

但似乎没有找到一些加载的模块并给出

Panic: Unbound name:
Relation.Binary.PropositionalEquality.Core.erefl[0,2,4,6,30]@ModuleNameHash
6189151057044369179
when retrieving the contents of a module

错误信息。在许多情况下，找到一个函数的定义而不是整个模块会很有帮助。

Answer 1

鼠标中键（适用于 Emacs）对我来说也不起作用。但是，您可以右键单击并选择“转到定义”，或者只需按 F12，它就会带您进入定义，因为您已经使用 C-c C-l 加载了文件。