相关疑难解决方法(0)

我已经定义了一个符号来模拟命令式样式编程

Notation "a >> b" := (b a) (at level 50).

然而,之后,所有函数应用程序表达式都表示为">>"样式.例如,在Coq Toplevel的证明模式中,我可以看到

bs' : nat >> list

实际上它应该是

bs' : list nat

为什么Coq积极地将所有函数应用程序样式表达式重写为我的自定义">>"表示？如何将一切恢复正常,我的意思是我想看到'a >> b'被解释为'ba'而'list nat'将不会被表示为'nat >> list'？

谢谢!