The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 25/08/2015 13:46, Dirk Pattinson wrote:

> I agree but am struggling to understand when sum and sumbool are applied
> to arguments of type Prop. In this case, it appears that both carry one
> bit of computational information: left or right, and the computational
> information of sum P Q (where P Q: Prop) isn't usable outside Prop, either.

A value of type "sumbool A B" carries a single bit of information. A 
value of type "sum A B" carries one bit of information or more 
(depending on whether values of types A and B carry any bit of 
information). This bit of information, for both sumbool and sum, can be 
used outside Prop, whether A and B are of type Prop or not. (It is the 
"or A B" type that does not carry any bit of information and thus cannot 
be destructed to get a value of a type outside Prop.)

> Differently put: assuming I'm not interested in extraction, could I
> replace "sumbool" by "sum" throughout (assuming I would be prepared to
> also do this in the libraries)?

Yes.

Definition sumbool : Prop -> Prop -> Set := sum.

Best regards,

Guillaume