The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Can someone explain to me why the type of [sum] is

      [Type (* Coq.Init.Datatypes.33 *) ->

       Type (* Coq.Init.Datatypes.34 *) ->

       Type (* max(Set, Coq.Init.Datatypes.33, Coq.Init.Datatypes.34) *)]

In particular, why is the [sum] of two propositions in [Set], rather than in [Prop]?

Thanks.

-Jason