Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Best explanation for simple type observation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Best explanation for simple type observation


Chronological Thread 
  • From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Best explanation for simple type observation
  • Date: Wed, 14 Jan 2015 11:22:07 -0500

Oh, there it is. Thank you. --Kevin

On Wed, Jan 14, 2015 at 11:02 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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

 

 





Archive powered by MHonArc 2.6.18.

Top of Page