在大多数 IDE 或文本编辑器中，您可以右键单击某个术语，它会将您带到定义该术语的文件。 CoqIDE好像没有这个，所以我一直在做coqdoc myfile.v --html，然后转到生成的 HTML 文档。但该文件中唯一可点击的术语是针对 Coq 标准库的。例如，由 ssreflect 定义的术语不可单击。
在 Coq 文件中，是否有一种标准方法能够快速查找定义某些术语/标识符（及其源代码）的位置？要么在 CoqIDE 中，要么在 emacs + ProofGeneral 中（我正在使用 CoqIDE，但如果 emacs/ProofGeneral 有这种能力，我会切换）。
或者是为您使用的每个 Coq 项目和依赖项生成文档的标准方法？
如果您突出显示一个术语，然后执行“查询”->“定位”，或者您评估Locate some_identifier.，您将获得常量的全名。如果您知道依赖项安装在哪里，这将告诉您在哪里查找标识符。
编辑：如果您想要标识符的定义，您可以Print它。如果你只想要它的类型，你可以使用About, or Check（它也接受表达式，而不仅仅是标识符）。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
