Это тип данных 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; Я рекомендую прочитать руководство об этом.