7

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

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

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

4

2 回答 2

6

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

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

于 2015-07-18T18:42:50.860 回答
3

在 Proof General 之上有一个工具，称为company-coq。默认情况下，它具有绑定到M-.键盘快捷键的跳转到定义功能。

Require只有当命令或其变体需要包含定义的模块时，它才能跳转到光标下的定义（甚至是标准库） 。

于 2018-01-18T21:00:22.493 回答