emacs - 如何高效地查找 Coq 中定义的标识符？

Question

在大多数 IDE 或文本编辑器中，您可以右键单击一个术语，它会将您带到定义该术语的文件。 CoqIDE 似乎没有，所以我一直在做 coqdoc myfile.v --html ，然后转到生成的 HTML 文档。但该文件中唯一可点击的术语是 Coq 标准库。 ssreflect 定义的术语(例如)不可点击。

在 Coq 文件中，是否有一种标准方法可以快速查找定义了某些术语/标识符(及其源代码)的位置？在 CoqIDE 或 emacs + ProofGeneral 中(我正在使用 CoqIDE，但如果 emacs/ProofGeneral 具有此功能，我会切换)。

或者是为您使用的每个 Coq 项目和依赖项生成文档的标准方法？

Answer 1

如果您突出显示一个术语，并执行查询 -> 定位，或者您评估 Locate some_identifier. ，您将获得常量的全名。如果您知道依赖项的安装位置，这将告诉您在哪里查找标识符。

编辑:如果你想要标识符的定义，你可以Print它。如果你只想要它的类型，你可以使用 About , 或 Check (它也接受表达式，而不仅仅是标识符)。