Как изменить стиль отображения в Coq IDE, чтобы он соответствовал Coqtop?

Импликационная связка печатается как лямбда-выражение в моем coqide (OS X El Capitan). это ожидаемое поведение? Я бы предпочел видеть их напечатанными, как в coqtop. Мне не удалось найти параметр / параметр командной строки для изменения стиля отображения.

coqtop and coqide


coq coqide
person Falcon    schedule 04.10.2016    source источник
comment
Проверьте запись в меню View -> Display notations.   -  person Anton Trunov    schedule 04.10.2016
comment
Спасибо! Я проверил это, когда делал снимки экрана, но каким-то образом переключение исправляет это.   -  person Falcon    schedule 04.10.2016
comment
Вы должны ответить, не поставив поле ответа;)   -  person Vinz    schedule 05.10.2016
comment
@Vinz Хорошо. Сделанный :)   -  person Anton Trunov    schedule 05.10.2016

Ответы (1)


arrow_upward
3
arrow_downward

Короткий ответ

Убедитесь, что в CoqIDE отмечен пункт меню Вид → Отображать нотации.

Длинный ответ

Coq по умолчанию красиво печатает, используя нотации.

Обозначение - это символическое сокращение, обозначающее какой-либо термин или шаблон термина.

Обозначение для -> определено в Coq.Init.Logic:

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

На этом можно сделать вывод, что Coq по какой-то причине разворачивает для вас нотации.

В coqtop (верхний уровень или REPL для Coq) или в ProofGeneral вы можете использовать команды Vernacular

Set Printing Notations.

и

Unset Printing Notations.

в ваших сценариях проверки для управления выводом (Set / Unset в приведенных выше командах можно читать как Use / Do not use).

К сожалению, в CoqIDE v8.5 они не работают: если вы попробуете, вы получите следующее сообщение об ошибке:

Так не пойдет. Вместо этого используйте меню дисплея CoqIDE

Я думаю, что единственный разумный вариант, который у нас есть, - это проверить пункт меню Вид → Отображать нотации.

person Anton Trunov    schedule 05.10.2016