coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] prod is still polymorphic over sort Type/Prop ?
Date: Mon, 19 Sep 2016 13:28:17 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb0-f180.google.com
Ironport-phdr: 9a23:ub4QABL8h1VOTlHg99mcpTZWNBhigK39O0sv0rFitYgULfrxwZ3uMQTl6Ol3ixeRBMOAuqsC27ad4vyoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMY2HHsPfsydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+vh7aCACL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOT8TbEvWTmhp45tQRnkwHMOPT4462HaiYp5iqtdrFSgpgBw64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5XAg==

(* checked in Coq versions 8.5pl1 and 8.5pl2 *)

Variable A:Prop.

Variable B:Prop.

Variable AT:Type.

Variable BT:Type.

Check (prod AT BT).

(* Type *)

Fail Check ((prod AT BT):Prop).

Check (A:Type).

Check ((prod A B)).

(* Prop

How is this justified?

I expected Type.

Check prod.

prod

: Type -> Type -> Type

Fail Check (AT:Prop).

-- Abhishek

[Coq-Club] prod is still polymorphic over sort Type/Prop ?, Abhishek Anand, 09/19/2016
- Re: [Coq-Club] prod is still polymorphic over sort Type/Prop ?, Matthieu Sozeau, 09/19/2016