问symbols /和||在Coq中代表什么？
EN

Stack Overflow用户

提问于 2015-05-03 15:45:52

回答 1查看 129关注 0票数 2

在coq中，符号/和||代表什么？我查了参考手册，在网上也找不到。

发布于 2015-05-03 18:25:56

这些符号(像大多数运算符一样)可以重新定义。这取决于上下文。

你可以通过问Coq得到最准确的答案。

例如，使用Locate "||".来显示包含标记||的所有当前符号。

如果您不确定在特定表达式中使用了哪种表示法，请让Coq将其重新打印出来，并禁用美观打印。

Unset Printing Notations.
Check (fun a b => a || b).
Set Printing Notations.

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/30011453

复制

相似问题

问symbols /和||在Coq中代表什么？EN