Избегайте печати обозначений в Coq с Proof General

Question

В лекции 6 DeepSpe c 2018, лектор проверяет определение

string_dec

, получая:

string_dec
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

Затем он продолжает видеть определение + , но раньше он отключает в CoqIde печать нотации. Так что сумбул напечатан. Этот последний символ можно проверить.

Как я могу сделать то же самое с Proof General?

Answer 1

Вы можете использовать меню, Coq > OPTIONS > Set Printing All.

Вы также можете напрямую выполнить команду, набрав Set Printing All. и оценив ее в своем буфере перед запуском команды Check. Это также дает вам доступ к Unset Printing Notations, чтобы отключить только печатные записи (что вы можете сделать с помощью меню в CoqIDE). Когда вы закончите, вы можете просто удалить эту команду, которая отменит ее эффект.

Наконец, вы также можете напрямую использовать Coq > OTHER QUERIES > Check (show all) на string_dec.