如何使用{

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