The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Kevin,

 

this is stated in chapter 4.3 (Conversion rules) in rule 4 in the paragraph “Convertibility” for the Prop to Set conversion. In the other direction this is implicitly stated by the lack of a conversion rule.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Kevin Sullivan
Sent: Wednesday, January 14, 2015 4:41 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Best explanation for simple type observation

 

Intuitively this should not work. And it doesn't.

    Inductive E: Set := .

    Definition p: Prop := E.

 

But this does.

    Inductive P: Prop := .

    Definition s: Set := P.

 

Can someone point me to the right part of the manual to determine how best to explain why?

 

KS