The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 16 Aug 2012 18:16:40 -0400,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> Can someone explain to me what is happening in the following code (in
> particular, in the last line)?  Is this a bug?
> 
> 
> Parameter foo : Type -> Type -> Type -> Type.
> Parameter bar : Type -> Type -> Type.
> 
> (* Notation "C ~ D" := (bar C D). (* Error: A left-recursive notation
> must have an explicit level. *) *)
> (* Notation "C .^{ M } D" := (foo C M D). (* Error: A left-recursive
> notation must have an explicit level. *) *)
> 
> Reserved Notation "C .^{ M } D" (at level 70, no associativity).
> Reserved Notation "C ~ D" (at level 70, no associativity).
> 
> Notation "C ~ D" := (bar C D). (* works fine *)
> (* Notation "C .^{ M } D" := (foo C M D) (at level 70, no
> associativity). (* would work fine *) *)
> Notation "C .^{ M } D" := (foo C M D). (* Error: A left-recursive
> notation must have an explicit level. *)
> 
> 
> 
> Thanks.
> 
> -Jason

I guess it is a bug. Replacing curly braces makes it work:

Reserved Notation "C .^« M } D" (at level 70, no associativity).
Notation "C .^« M } D" := (foo C M D).

Reserved Notation "C .^{ M » D" (at level 70, no associativity).
Notation "C .^{ M » D" := (foo C M D).



Reserved Notation "C { M } D" (at level 70, no associativity).
Does not work either, and intertingly reports that '{' and '}' are not
considered as symbols. I tried to escape them between (single) quotes,
but it did not work either.

This also works :

Reserved Notation "C .^{ M .^} D" (at level 70, no associativity).
Notation "C .^{ M .^} D" := (foo C M D).

But this does not:

Reserved Notation "C .^{ M }^. D" (at level 70, no associativity).
Notation "C .^{ M }^. D" := (foo C M D).


So use of curly braces seems to be following some particular rule.
I do not remember this in the documentation, and I believe that braces
in Notations used to work…