coq - 在 Coq-IDE 中浏览定义

Question

在 Isabelle 证明助手中，可以单击 Ctrl+单击一个术语，IDE 会将他重定向到相关定义。

这可以用 CoqIde 完成吗？与证明一般？

Answer 1

是的，您在帖子和评论中提到的功能（顺便说一句，请随时编辑您的问题以合并您的评论）在Proof-General和/或company-coq（收集 Proof 的 IDE 扩展的 Emacs 包）中是可能的-一般的）：

• 查看定义的内容def（相当于Print def.）：C-c C-a C-p def RET
• 查看定义的类型def（相当于Check def.）：C-c C-a C-c def RET
• 查看定义的类型和相关元数据def（相当于About def.）：C-c C-a C-b def RET
• 一次性查看所有这些点下的标识符（需要company-coq）：C-c C-d
• 被重定向到点下定义的位置（需要company-coq）：M-.
• 使 point 下的定义在不移动的情况下显示出来（需要company-coq）：<C-down-mouse-1>

提醒

为了独立起见，Emacs 键绑定C-c, M-., RET,<C-down-mouse-1>指的是Ctrl+c, Alt+., Return, and Ctrl+click（不释放鼠标按钮）。

最后，您可以通过以下方式发现与环境模式关联的绑定列表C-h m：

C-h k [describe-key] C-h m [describe-mode]：

C-h m runs the command describe-mode (found in global-map), which is
an interactive compiled Lisp function in ‘help.el’.

It is bound to C-h m, <f1> m, <help> m, <menu-bar> <help-menu>
<describe> <describe-mode>.

(describe-mode &optional BUFFER)

Display documentation of current major mode and minor modes.
A brief summary of the minor modes comes first, followed by the
major mode description.  This is followed by detailed
descriptions of the minor modes, each on a separate page.

[…]