我在Coq中的两个命题（可能是类型）之间与plus运算符作斗争。我已经可以弄清楚这是“或”（也许是“ xor”）之类的东西，并且我认为它是可以确定的，但我无法理解它的完整含义，并且该符号从何而来（在经典数学中）。
P。 S.当然，我已经谷歌搜索和研究，但是找不到我想要的完整复杂的答案。
这是sum数据类型，其中sum基本上是A + B或A。与B的主要区别在于它位于A \/ B中，因此具有计算内容。也就是说，在给定Type的情况下，您不能产生使A \/ B如此的布尔值。
另一种查看方式是，对于if A then true else false，A B : Prop成立，但反之则不成立。
A + B -> A \/ B是Coq中的一种特殊的命令性排序；我建议阅读有关它的手册。