The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Actually,

Check eq S0 P0 .

produces

S0 = P0
     : Prop

Is this a bug?

V.




On Oct 13, 2009, at 1:49 PM, Vladimir Voevodsky wrote:

> In the following sequence of instructions:
>
> Axiom f5 : Set -> nat .
>
> Axiom P0 : Prop .
>
> Axiom S0 : Set .
>
> Check f5 P0 .
>
> Check eq P0 S0 .
>
> The last two produce the following reactions:
>
> f5 P0
>     : nat
>
> and
>
> Error: The term "S0" has type "Set" while it is expected to have  
> type "Prop".
>
> respectively.
>
> Why does f5 treat Prop as a subtype of Set but eq does not?
>
> V.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club