Coq表示法中的`<`语法错误

Question

以下代码:

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

给出以下错误:

Syntax error: '<' expected after [constr:operconstr level 200] (in [constr:operconstr])

如果我用<:它代替,我会收到类似的错误<.

但是这段代码运行正常:

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

为什么？是否有可以更改为允许<或<:以符号表示的优先级设置？是否存在我正在与之碰撞的内置语法,并且在定义符号时需要注意？

Answer 1

Coq使用LL1解析器来处理符号.它还可以输出语法.所以,让我们通过以下内容检查我们得到了什么

Reserved Notation "g || t |- x < y" (at level 10).

Print Grammar constr. 输出:

...
| "10" LEFTA
  [ SELF;
    "||";
    constr:operconstr LEVEL "200";        (* subexpression t *)
    "|-";
    constr:operconstr LEVEL "200";        (* subexpression x *)
    "<";
    NEXT
...

这里,

• 10 是我们的优先级别;
• LEFTA 意味着左联合;
• 200 是内部子表达式的默认优先级.

考虑到较低级别比较高级别更紧密地绑定的事实以及级别<为70(参见Coq.Init.Notations)的事实,我们可以推断出Coq正试图将该x < y部分解析为子表达式,从而x消耗该<令牌,因此错误消息.

为了解决这种情况,我们可以通过指定x更高的优先级,即更低的级别,明确禁止将第三个参数解析为小于表达式.

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