Coq + Emacs？`‘Emacs`’看不到源文件中定义的内容。

Question

因此，我正在使用Coq使用Emacs作为IDE。proof-general和company-coq都已正确安装和加载。

然后打开虚拟whatever_name.v文件并使用Fixpoint关键字定义递归函数。

然后我在上面运行coq-Check并得到：

检查addnm。

错误:在当前环境中找不到参考地址not。

但是，例如，Inductive unit : Set := tt.运行得非常好。

我做错了什么？

​

​

Answer 1

我的印象是，你没有要求Coq阅读addnm的定义。尝试在Coq缓冲区上按C-c C-n。这应该指示将下一个命令发送到Coq进行处理。当命令被发送时，您应该看到您的缓冲区逐渐转到不同的颜色。一旦突出显示了addnm的定义，您应该能够检查它(C-c C-a C-c)。

( unit仍然工作的原因是它的定义在Emacs中启动Coq时会自动加载。)