notation - 如何在 Coq 中使用 { 定义 Notation 格式

Question

我定义了这个符号：

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 } "). 

在这种情况下，我得到

警告：标识符“{”开头的字符“{”无效。

那么我应该如何使用 { 定义格式？

Answer 1

只需从格式中删除花括号：

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 ]).