0

我正在关注 cpdt ( http://adam.chlipala.net/cpdt/html/Universes.html ) 中的 Universes 章节，该章节运行Set Printing Universes.以查看有关类型的其他评论。但是，我正在运行 CoqIde 8.6，它没有任何效果。

以下代码

Set Printing Universes.
Check Type.

输出

Type
    : Type

而这本书说它应该输出

Type (* Top.3 *)
     : Type (* (Top.3)+1 *)

我错过了一些命令吗？我应该使用不同版本的 Coq 吗？

编辑：我只是在命令行中尝试了这个，coqtop它确实打印了类型注释。也许我必须在 CoqIDE 中启用一些额外的选项？

4

1 回答 1

1

是的，CoqIde 对此有一个特定的菜单：“查看”>“显示宇宙级别”。您可以从“查看”菜单访问许多其他设置，但它们的对应命令（Unset Printing Notations.等）对 CoqIde 无效。

于 2018-02-04T12:08:26.060 回答