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