Что означает оператор «+» между двумя предложениями в Coq - PullRequest
2 голосов
/ 24 марта 2020

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

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

1 Ответ

4 голосов
/ 24 марта 2020

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

...