The Coq mailing list

["N. Raghavendra" <nyraghu27132 AT gmail.com>]

At 2017-12-02T17:17:44+01:00, Hugo Herbelin wrote:

> I'll try to give some explanation.

Dear Hugo,

Many thanks for your detailed explanation.

>> Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 
>> 99).
>>
>> So, what does attaching the precedence level 99 to x, which is not
>> an operator, mean?
>
> By asking to parse x at level "99", we tell to (prioritarily) parse
> the expression following "{" in "{ x : A | P }" at level "99", and, by
> doing so, this excludes parsing "t : u" (i.e. rule « SELF; ":"; SELF »)
> which is at level "100".

I understand that now.  My mistake was in associating precedence levels
with operations alone, and not realising that it makes sense to
associate them also with other elements of expressions involving these
operations.

>> How does it ensure that "x : A" is not confused with a type cast, as
>> mentioned in the manual?
>
> By excluding level "100", an expression "t : u" is then (prioritarily)
> parsed by the "x : A" part of the rule "{ x : A | P }" (which itself
> shows as
>
> | "{"; constr:operconstr LEVEL "99"; "|"; constr:operconstr LEVEL "200";
>     "&"; constr:operconstr LEVEL "200"; "}"
>
> with "Print Grammar constr.") rather than by the rule « SELF; ":"; SELF »
> which is at level 100.

Yes, that is clear.

>> Reserved Notation "x -> y" (at level 99, right associativity, y at level 
>> 200).
>>
>> Is there a reason, as in the above example, to choose 200 for y?
>
> This is a more complicated question. Strictly speaking, the
> primary reason is that we want to parse things like, say,
> "x < y -> forall z, y < z -> x < z" and that the rule for
> "forall z, ..." is (indirectly, via an entry called "binder_constr")
> at level "200" (as "Print Grammar constr." would show).

Also, because "A -> B" is a notation for "forall (_ : A), B", it perhaps
makes sense to assign the y in the expression "x -> y" the same
precedence level as the y in the expression "forall (x : _), y", which
according to `Print Grammar constr.', seems to be 200.

Thanks again for your helpful explanation.

Best regards,
Raghu.

--
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/