Что означает оператор «+» между двумя предложениями в Coq

Question

Я борюсь с оператором плюс между двумя предложениями (возможно, типами) в Coq. Я уже мог понять, что это что-то вроде «или» (может быть, «xor»), и я думаю, что это говорит о том, что что-то решаемо, но я не могу понять полный смысл этого и откуда взялся этот знак (в классической математике).

PS Конечно, я уже гуглил и исследовал, но не смог найти полный сложный ответ, который я хочу.

Answer 1

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