The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

If you do "Print Grammar constr", you will see that the notation for
sigT follow the following rule:

...
| "0" LEFTA
  [ "{"; constr:operconstr LEVEL "99"; ":"; constr:operconstr LEVEL "200";
    "&"; constr:operconstr LEVEL "200"; "&"; constr:operconstr LEVEL "200";
    "}"
...

Because the underlying parser of Coq, which is camlp4/camlp5, is
basically an LL parser, rules have to be factorized by hand.

To get this factorization, you need to put any notation starting with
"{" at level 0, and with first expression being parsed at level
99. This gives:

Notation "{ A , .. , B }" := (cons A .. (cons B nil) ..) (at level 0, A at 
level 99).

This will not hide the notation for sigT but this will break the
notation sumbool though, because "{ A } + { B }" will not be parsed
any longer as a sumbool but as some "+" of singleton lists "{A}" and
"{B}". So maybe, you would prefer to use the notation:

Notation "{ A , B , .. , C }" := (cons A (cons B .. (cons C nil) ..)) (at 
level 0, A at level 99).

and to write differently the lists of one element.

Note that it might be wise to set the parsing level for B at 99 too,
depending on whether interferences are likely to happen with other
notations involving ",".

Hope this helps.

Hugo Herbelin

On Thu, Dec 20, 2012 at 02:29:56PM -0500, Gregory Bush wrote:
> In the following example, is there a modifier I can use when
> declaring the notation so it doesn't hide the notation for sigT?
> 
> Require Import List.
> 
> (* So far so good *)
> 
> Check {x : nat & {y | x < y}}.
> 
> Notation "{ A , .. , B }" := (cons A .. (cons B nil) ..).
> 
> (* Oops *)
> 
> Check {x : nat & {y | x < y}}.