Установка юниверсов печати не влияет

Я следую главе «Вселенные» в cpdt (http://adam.chlipala.net/cpdt/html/Universes.html), который запускает Set Printing Universes. для просмотра дополнительных комментариев к типам. Однако я использую CoqIde 8.6, и это не дает никакого эффекта.

Следующий код

Set Printing Universes.
Check Type.

выходы

Type
    : Type

в то время как в книге говорится, что он должен выводить

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

Я пропустил какую-то команду? Должен ли я использовать другую версию Coq?

РЕДАКТИРОВАТЬ: я только что попробовал это в командной строке с coqtop, и он печатает аннотации типа. Может быть, мне нужно включить какую-то дополнительную опцию в CoqIDE?


coq coqide
person Community    schedule 03.02.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Да, в CoqIde для этого есть специальное меню: «Вид» > «Отображать уровни вселенной». Существует довольно много других настроек, к которым вы можете получить доступ из меню «Вид», но их аналогичная команда (Unset Printing Notations. и т. д.) не влияет на CoqIde.

person mpetruska    schedule 04.02.2018