Coq 表示法中带有 `<` 的语法错误答案

【问题标题】：Syntax Error with `<` in Coq NotationsCoq 表示法中带有 `<` 的语法错误
【发布时间】：2017-07-03 12:13:32
【问题描述】：

以下代码：

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

为什么？是否可以更改优先设置以允许< 或<: 使用符号？是否有我遇到的内置语法，并且在定义符号时需要注意？

【问题讨论】：

标签： parsing syntax operators coq notation

【解决方案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 正在尝试解析@987654330 @ 部分作为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

【讨论】：