The Coq mailing list

[Gregory Bush <gbush AT mysck.com>]

Thank you for the response.

The (at level 0, A at level 99) notation was one I tried, but I did  
not work in my environment either (8.2 .. a bit old)  However, it does  
give different results, in that coqide highlights the colon instead of  
the ampersand as the location of the parsing error.

(Another quirk was when I tried Print Grammar constr, coqide did not  
seem to display any useful information, but I just discovered that it  
was all logged to my terminal window, so that is good to know for next  
time.)

I don't really need to talk about singletons in the theory I'm working  
with and the { A , B , .. , C } notation seems to work fine, so I will  
try that suggestion instead.

On Dec 20, 2012, at 2:59 PM, Hugo Herbelin wrote:

> 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}}.