How to define Notation format in Coq using {

Question

I defined this notation:

Definition Id (n:nat):= n.

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

Which works just fine. Now I want to add format to change the line breaks and alignment. Suppose I want to Print something like this:

ID
 { n }

So I tried the following notation:

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

In which case I get

Warning: Invalid character '{' at beginning of identifier "{".

So How am I supposed to define a format using {?

Answer 1

Simply remove the curly braces from the format:

Definition Id (n : nat) := n.

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

Check (ID { 4 }).

I'm not sure this is intentional or a bug. However, as the Coq user's manual says, curly braces { } have a special status in notations and are treated differently from other kinds braces. Thus, if you want to do the same with, say, [ ], you need to include the brackets in the format:

Definition Id (n : nat) := n.

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

Check (ID [ 4 ]).