如何解决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
在左端的词条上。)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。