Syntax error with `<` in Coq Notation
The following code:
Reserved Notation "g || t |- x < y" (at level 10). Inductive SubtypeOf : GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set := | SubRefl : forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u < u where "g || t |- x < y" := (SubtypeOf g t x y).
gives the following error:
Syntax error: '<' expected after [constr:operconstr level 200] (in [constr:operconstr])
You get a similar error if you <
use <:
.
But this code works great:
Reserved Notation "g || t |- x << y" (at level 10). Inductive SubtypeOf : GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set := | SubRefl : forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u << u where "g || t |- x << y" := (SubtypeOf g t x y).
Why? Is there a priority setting that can be changed to allow <
or <:
in notation? Is there a built-in syntax that I am running into that I need to watch out for when defining notation?
source share
Coq uses the LL1 parser for notation processing. It can also output grammar. So let's see what happened with the following
Reserved Notation "g || t |- x < y" (at level 10).
Print Grammar constr.
outputs:
... | "10" LEFTA [ SELF; "||"; constr:operconstr LEVEL "200"; (* subexpression t *) "|-"; constr:operconstr LEVEL "200"; (* subexpression x *) "<"; NEXT ...
Here
-
10
- our priority level; -
LEFTA
means left associativity; -
200
is the default precedence level for inner subexpressions.
Considering the fact that the lower level is bound more tightly than the higher one, and the fact that the level <
is 70 (see Coq.Init.Notations
), we can conclude that Coq is trying to parse the part x < y
as a subexpression for x
, consuming the token <
, hence the message about the error.
To remedy the situation, we can explicitly disallow parsing of the third parameter as a smaller expression by assigning x
a higher priority, i.e. lower level.
Reserved Notation "g || t |- x < y" (at level 10, x at level 69). Print Grammar constr. | "10" LEFTA [ SELF; "||"; constr:operconstr LEVEL "200"; (* subexpression t *) "|-"; constr:operconstr LEVEL "69"; (* subexpression x *) "<"; NEXT
source share