如何更改 Coq IDE 中的显示样式以匹配 Coqtop？
How to change display style in Coq IDE to match Coqtop?
蕴涵连接词在我的 coqide (OS X El Capitan) 中打印为 lambda 表达式。那是预期的行为吗？我更愿意看到它们打印成 coqtop。我找不到 option/command 行选项来更改显示样式。
简答
确保在 CoqIDE 中选中 View → Display notations 菜单条目。
长答案
默认情况下，Coq 使用符号漂亮地打印内容。
A notation is a symbolic abbreviation denoting some term or term pattern.
-> 的表示法在 Coq.Init.Logic 中定义：
Notation "A -> B" := (forall (_ : A), B) : type_scope.
此时我们可以得出结论，Coq 出于某种原因正在为您展开符号。
在 'coqtop'（顶层，或 Coq 的 REPL）或 ProofGeneral 中，您可以使用 Vernacular 命令
Set Printing Notations.
和
Unset Printing Notations.
在您的证明脚本中控制输出（可以将上面命令中的 Set / Unset 读为 Use / Do not use）。
不幸的是，这些在 CoqIDE v8.5 中不起作用：如果您尝试，您将收到以下错误消息：
This will not work. Use CoqIDE display menu instead
我想我们唯一合理的选择是检查 View → Display notations 菜单项。
蕴涵连接词在我的 coqide (OS X El Capitan) 中打印为 lambda 表达式。那是预期的行为吗？我更愿意看到它们打印成 coqtop。我找不到 option/command 行选项来更改显示样式。
简答
确保在 CoqIDE 中选中 View → Display notations 菜单条目。
长答案
默认情况下，Coq 使用符号漂亮地打印内容。
A notation is a symbolic abbreviation denoting some term or term pattern.
-> 的表示法在 Coq.Init.Logic 中定义：
Notation "A -> B" := (forall (_ : A), B) : type_scope.
此时我们可以得出结论，Coq 出于某种原因正在为您展开符号。
在 'coqtop'（顶层，或 Coq 的 REPL）或 ProofGeneral 中，您可以使用 Vernacular 命令
Set Printing Notations.
和
Unset Printing Notations.
在您的证明脚本中控制输出（可以将上面命令中的 Set / Unset 读为 Use / Do not use）。
不幸的是，这些在 CoqIDE v8.5 中不起作用：如果您尝试，您将收到以下错误消息：
This will not work. Use CoqIDE display menu instead
我想我们唯一合理的选择是检查 View → Display notations 菜单项。