coq - 如何更改 Coq IDE 中的显示样式以匹配 Coqtop？

Question

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

score 3 · Accepted Answer

简短的回答

确保在 CoqIDE 中选中了View → Display notations菜单条目。

默认情况下，Coq 使用符号漂亮地打印内容。

符号是表示某些术语或术语模式的符号缩写。

的符号->在Coq.Init.Logic中定义：

Notation "A -> B" := (forall (_ : A), B) : type_scope.

在这一点上，我们可以得出结论，Coq 出于某种原因正在为您展开符号。

在“coqtop”（一个顶层，或 Coq 的 REPL）或ProofGeneral中，您可以使用 Vernacular 命令

Set Printing Notations.

和

Unset Printing Notations.

在您的证明脚本中控制输出（可以在上面的命令中将 / 读取为/ Set）。UnsetUseDo not use

不幸的是，这些在 CoqIDE v8.5 中不起作用：如果您尝试，您将收到以下错误消息：

这行不通。改用 CoqIDE 显示菜单

我想我们唯一合理的选择是检查View → Display notations菜单项。