Как определить формат нотации в Coq с помощью {

Я определил это обозначение:

Definition Id (n:nat):= n.

Notation "'ID' { n } ":= (Id n) (no associativity, at level 99).

Что отлично работает. Теперь я хочу добавить формат, чтобы изменить разрывы строк и выравнивание. Предположим, я хочу напечатать что-то вроде этого:

ID
 { n }

Поэтому я попробовал использовать следующие обозначения:

Notation "'ID' { n } ":= (Id n) (no associativity, at level 99, 
format "'ID' '//' { n } ").

В этом случае я получаю

Предупреждение: недопустимый символ '{' в начале идентификатора "{".

Итак, как мне определить формат с помощью {?


notation coq
person user2506946    schedule 20.06.2013    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Просто удалите фигурные скобки из формата:

Definition Id (n : nat) := n.

Notation "'ID' { n } " := (Id n)
                            (no associativity, at level 99,
                             format "'ID' '//'  n  " ).

Check (ID { 4 }).

Я не уверен, что это намеренно или ошибка. Однако, как сказано в руководстве пользователя Coq, фигурные скобки { } имеют особый статус в обозначениях и обрабатываются иначе, чем другие виды фигурных скобок. Таким образом, если вы хотите сделать то же самое, скажем, с [ ], вам необходимо включить скобки в формате:

Definition Id (n : nat) := n.

Notation "'ID' [ n ] " := (Id n)
                            (no associativity, at level 99,
                             format "'ID' '//'  [ n ] " ).

Check (ID [ 4 ]).
person Arthur Azevedo De Amorim    schedule 24.06.2013