我在Coq中的两个命题（可能是类型）之间使用plus运算符而苦苦挣扎。我已经可以弄清楚这是“或”（也许是“ xor”）之类的东西，并且我认为它是可以确定的，但我无法理解它的完整含义，并且该符号来自何处（在经典数学中）。
PS当然，我已经用Google搜索和研究了，但是找不到我想要的完整复杂的答案。
这就是sum数据类型，A + B基本上是A或B。与的主要区别A \/ B在于它位于中Type，因此具有计算内容。就是说，鉴于A \/ B您不能产生这样的布尔值if A then true else false。
看到它的另一种方式是，对A B : Prop，A + B -> A \/ B持有，而不是相反。
Prop在Coq中是一种特殊的，强制性的类别；我建议阅读有关它的手册。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句