The Coq mailing list

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

I am reading Section 12.1.3 (Complex notations) of the manual, which has
the example

Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99).

My understanding was that one attaches precedence levels to operations
(as in "* has a higher precedence level than +").  So, what does
attaching the precedence level 99 to x, which is not an operator, mean?
How does it ensure that "x : A" is not confused with a type cast, as
mentioned in the manual?

On a related note, Coq.Init.Notations declares

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?

Thanks and regards,
Raghu.

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