如何使用來定義勒柯克符號格式{

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 user's manual所述，大括號{ }在符號中具有特殊的地位，並且與其他類型的大括號不同。因此，如果您想要對[ ]執行相同操作，則需要在格式中包含括號：

Definition Id (n : nat) := n. 

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

Check (ID [ 4 ]).