我定义了这个符号：
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 } ").
在这种情况下我会得到
警告：标识符“{”开头的字符“{”无效。
那么我应该如何使用 { 来定义格式？
【问题讨论】：
只需从格式中删除花括号：
Definition Id (n : nat) := n.
Notation "'ID' { n } " := (Id n)
(no associativity, at level 99,
format "'ID' '//' n " ).
Check (ID { 4 }).
我不确定这是故意还是错误。然而，正如Coq user's manual 所说，花括号{ } 在符号中具有特殊的地位，并且与其他类型的花括号区别对待。因此，如果你想对[ ] 做同样的事情，你需要在格式中包含括号：
Definition Id (n : nat) := n.
Notation "'ID' [ n ] " := (Id n)
(no associativity, at level 99,
format "'ID' '//' [ n ] " ).
Check (ID [ 4 ]).
【讨论】：