Coq-IDE中的浏览定义

Question

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

可以用CoqIde完成吗？有普通证明吗？

Answer 1

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

• 以查看定义def（等同于Print def.）的内容：C-c C-a C-p def RET
• 以查看定义Print def.的类型（等同于def）：C-c C-a C-c def RET
• 以查看定义Check def.（等同于Check def.）的类型和相关元数据：C-c C-a C-b def RET
• 一眼就能看到所有这些，以找到要点下的标识符（需要company-coq）：C-c C-d
• 将重定向到点下的定义位置（需要company-coq）：M-。
• 使点下的定义显示不动（需要company-coq）：

提醒

仅是自包含的，Emacs键绑定Cc，M-。，RET，仅指 Ctrl + c，Alt +。，Return和Ctrl + click（无需释放鼠标按钮）。

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

C-h kdefC-h m About def.：

About def.