问题标签 [coqide]

我是 Coq 的新手，从事集合论证明写作。

我意识到括号被省略了，我很难阅读公式。例如，

但我希望 Coq 打印(A :\: A) :|: (A :&: B) = B. 上面的输出是通过以下代码获得的。

令我惊讶的是，如果我看到finset.vsetDDr的原始编码，它的括号如下

所以我想知道为什么括号会消失，以及如何强制 Coq 在 CoqIde 中显式打印括号。

coqide蕴涵连接词在我的(OS X El Capitan)中打印为 lambda 表达式。这是预期的行为吗？我更希望看到它们以coqtop. 我找不到更改显示样式的选项/命令行选项。

我正在使用 CoqIDE 来完成 Software Foundations 书中关于 Coq 的练习。我可以成功编译 Basics.v，从而在我的目录中生成 Basics.vo 和 Basics.glob。当我尝试运行 Induction.v 时，它可以工作。当我尝试编译它时，它抱怨大量缺少引用，例如evenband negb_involutive。如果我将 Basics.v 内容复制到 Induction.v 中，它会编译，但显然这不是要走的路。

这不是问题Coq error: The reference evenb was not found in the current environment的重复，因为我已经做了这些事情：

编译基础.v。检查 Basics.vo 是否在目录中。现在编译 Induction.v。这最后一步失败了。

我使用 OpenSuse Leap，并从源代码构建 Coq-8.5。但是在 coqide 和偏好中没有语法着色，我不能选择语言：

在控制台输出中，我只有：

像libgtksourceview我安装的所有库。

我遇到了一个奇怪的问题......最近我在使用 CoqIDE 时遇到了一些奇怪的情况，即：

1. 如果不按住 windows/super 键，我无法输入字母“v”。

2. 如果打开了多个窗口，按退格键会将焦点移至上一个选项卡，我无法使用它删除内容。CTRL+退格键虽然适用于删除块。

两者中的第一个（可能已经发生）发生在我将键盘映射从 US 更改为 GB 之后，但来回切换并没有解决问题。

运行 ARCH linux，一切都是最新的，没有其他应用程序受到影响，我没有粘滞键。

感谢您的任何建议！

编辑：尝试重新安装，没有帮助...

已解决的编辑：是的，你完全正确，我似乎在没有注意到的情况下做了一些超快速的重新绑定。我还了解到，包管理器基本上不会接触 .config 文件，因为它们是由应用程序生成的，因此不受管理器的管辖。解决了！

与 Agda 不同，Coq 倾向于将证明与函数分开。Coq 给出的策略非常适合编写证明，但我想知道是否有一种方法可以复制一些 Agda 模式的功能。

具体来说，我想：

• 相当于 Agda?或 Haskell 的_，我可以在编写函数时省略部分函数，​​并且（希望）让 Coq 告诉我需要放在那里的类型
• 相当于 Agda 模式 (reify) 中的 Cc Cr，您可以在其中?使用函数填充块，它会?为所需的参数创建新块
• 当我match在一个函数中执行一个函数时，让 Coq 自动编写扩展可能的分支（如 Agda 模式中的 Cc Ca）

在 CoqIde 或 Proof General 中这可能吗？

我一直在使用来自https://coq.inria.fr/的下载链接为 Windows 和 Mac 安装 Coq。但是，当我尝试coqc或coqtop在终端或命令提示符上时，我收到错误消息，提示找不到该命令。尽管话虽如此，但我仍然可以在 Coq IDE 上几乎完美地运行 Coq，但是当我编译缓冲区时，尤其是来自Software Foundations的练习时，我收到以下消息。

据我了解，这2>&1似乎是某种形式的误导，我觉得这就是为什么coqc并且coqtop似乎在我的终端/命令提示符上不起作用的原因。

有人可以建议在 Mac 或 Windows 或两者上安装 Coq 的“最佳”方法，这样我就不会遇到上面提到的问题吗？

默认的相对面板宽度是 50% 输入和 50% 其他面板。如何以编程方式将其更改为例如 70/30？我在 Linux 上有 Coq(IDE) 8.5

我正在使用自动 Coq 8.5 生成文件生成器。这个 makefile 以“Top”作为所有模块的前缀。. 现在假设您通过 make 运行了很多文件，然后想要在 IDE 中更改/调试某些文件。然后令人讨厌的事实是 Coq 抱怨它无法找到已编译的其他文件，因为在 IDE 中它假定名称没有“Top”前缀。我试图调整 makefile 以摆脱这个前缀。但我总是以一些错误信息结束。有人可以告诉我如何删除 make 中的“Top”前缀或告诉 IDE 使用“Top”前缀。

I have a fresh install of Coq 8.6 in Ubuntu 17.04. When I try to compile my project using make, it works fine until I get the first error message. Then, I try to use CoqIDE to locate and correct the error, but I get new error messages, such as:

"The file foo.vo contains library Top.foo and not library foo"

My guess is that something is wrong with the configuration of CoqIDE, but I do not know what that could be. Any hints?

Thanks in advance, Marcus.