The Coq mailing list

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

Yes, it does not work in 8.2 because 8.2 is lacking an automatic
expansion strategy of

Notation "{ A , .. , B }" := (cons A .. (cons B nil) ..).

into 

Notation "{ A }" := (cons A nil).
Notation "{ A , B , .. , C }" := (cons A (cons B .. (cons C nil) ..)).

so as to keep factorization with rules starting with "{ A". This
automatic expansion strategy has been introduced in 8.3.  If you do
the expansion by hand, it will work (what apparently you're going to
do anyway according to the rest of your message).

Hugo Herbelin

On Thu, Dec 20, 2012 at 03:33:54PM -0500, Gregory Bush wrote:
> 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}}.