coq - Coq 中的“下一个级别”？

Question

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

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

其中 xform 是介于两者之间的函数。

标签： coqcoq-tactic

Answer 1

Consider a ->> b ->> c. There are two ways to parse it, either t1 is a and t2 is b ->> c, or t1 is a ->> b and t2 is c. Because t2 is marked at next level, only a notation with a level lower than 69 can be used in there, which makes b ->> c impossible (unless parenthesized). So, a ->> b ->> c is parsed as (a ->> b) ->> c.

Note that t2 at next level is redundant in the above notation. Indeed, attribute left associative already forces at next level on the term at the right end. (While right associativity forces at next level on the term at the left end.)