coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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
- [Coq-Club] Best explanation for simple type observation, Kevin Sullivan, 01/14/2015
- RE: [Coq-Club] Best explanation for simple type observation, Soegtrop, Michael, 01/14/2015
- Re: [Coq-Club] Best explanation for simple type observation, Kevin Sullivan, 01/14/2015
- RE: [Coq-Club] Best explanation for simple type observation, Soegtrop, Michael, 01/14/2015
Archive powered by MHonArc 2.6.18.