Hoare тройная запись

Question

Недавнее обсуждение нотаций множеств побуждает меня спросить, есть ли у кого-нибудь (Tej?) Умная идея заставить Coq принять стандартную нотацию для троек Хоара - что-то вроде этого:

Notation "{ P }  c  { Q }" :=
  (hoare_triple P c Q) 
  (at level 0, P at level 99, c at level 99, Q at level 99) 
  : Hoare_scope.

Ошибка Coq: «Ошибка: нотация должна содержать хотя бы один символ». Что я не понимаю в свете того факта, что

Notation "{ x }" := (x) (at level 0, x at level 99).

работает.

Любой совет?

Answer 1

Я бы порекомендовал использовать другой символ где-нибудь, чтобы сделать это разбираемым Я видел, как Адам Чипала использовал Notation "{{ P }} c {{ Q }}", например. Вы также можете определить { P } c { Q } как нотацию только для печати, хотя я думаю, что это менее полезно и потенциально запутывает новых пользователей.

фигурные скобки являются специальными; * Некоторые из этих особенностей задокументированы в руководстве (прокрутите вниз до третьей заметки), но, признаюсь, я не совсем понимаю эту заметку за пределами того, что "здесь будут драконы, спросите Хьюго Гербелина".

Я могу сказать вам механически, почему вы получаете сообщение об ошибке, в то время как "{x}" работает:

• фигурные скобки не считаются символами из-за специальной remove_curly_brackets функции
• если нотация уже есть в таблице синтаксического анализа, нет необходимости включать новые символы

Это проверено в metasyntax.ml , который я нашел, посмотрев, как выдается сообщение об ошибке. Вы также можете подтвердить, что использует грамматика Coq Print Grammar constr (это также, как вы выясняете, на каком уровне все на самом деле).