Coq表示法中带有<`的语法错误 [英] Syntax Error with `<` in Coq Notations

问题描述

以下代码:

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

如果我使用<:代替<，也会收到类似的错误.

I get a similar error if I use <: in place of <.

但是此代码可以正常工作:

But this code works fine:

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 precedence setting that can be changed to allow < or <: in notation? Is there built-in syntax that I'm colliding with, and need to watch for when defining notations?

推荐答案

Coq使用LL1解析器来处理符号.它还可以输出语法.因此，让我们检查以下内容

Coq uses an LL1 parser to process notations. It also can output the grammar. So, let's check what we are getting with the following

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是内部子表达式的默认优先级.

• 10 is our precedence level;
• LEFTA means left associativity;
• 200 is the default precedence level for inner subexpressions.

考虑到较低的级别比较高的级别绑定更紧密的事实以及<的级别为70的事实(请参阅

Taking into account the fact that a lower level binds more tightly than a higher level and the fact that the level of < is 70 (see Coq.Init.Notations), we can deduce that Coq is trying to parse the x < y part as a subexpression for x, consuming the < token, hence the error message.

为解决这种情况，我们可以通过分配x较高的优先级(即较低的优先级)来明确禁止将第三个参数解析为小于表达式.

To remedy the situation we can explicitly disallow parsing the third parameter as the less-than expression by assigning x higher precedence, i.e. a 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

这篇关于Coq表示法中带有<`的语法错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！