Coq中的“下一级别”？

问题描述

以下表示法中的“下一个级别”位是什么意思（假设已经指定了级别）：

Reserved Notation "t1 ->> t2" (left associativity,at level 69,t2 at next level). 
...
where "t1 ->> t2" := (xform t1 t2).

其中xform是在两者之间定义的函数。

解决方法

考虑a ->> b ->> c。有两种解析方法，t1是a和t2是b ->> c，或者t1是a ->> b和{{1} }是t2。由于c被标记为t2，因此只能在其中使用级别低于at next level的符号，这使得69不可能（除非带括号）。因此，b ->> c被解析为a ->> b ->> c。

请注意，(a ->> b) ->> c在上述符号中是多余的。实际上，属性t2 at next level已经在右边的项上强制left associative。 （虽然at next level迫使right associativity在左端的词条上。）