coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] why Prop appears?

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Adam Chlipala <adam AT chlipala.net>
Cc: Loic Pottier <loic.pottier AT inria.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] why Prop appears?
Date: Tue, 14 Dec 2010 16:11:22 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=D/27x5NC63XbJbkxZXANXu3YTh8cKHQ00maLtvRWHIErM4iK+Lj8+paKQRmNkiGajR hosC1i3v676nF8uoGzNp8JaUxGWLupHGHPEMiONwyCZx+fc7UVojkYuM8zN5Jj2JMT+J Ei3fRB1MmrQ5nQjwEXOkiEe/ilkK7vL3M8vZE=

2010/12/14 Adam Chlipala
<adam AT chlipala.net>:
>
> I think this is the simulated universe polymorphism. �Coq detects that your
> definition could just as well be put in [Prop], and doing so only increases
> the set of valid contexts where your type could be used. �Thus, the change
> happens automatically.

And if you want it in type, you can :
Check ((forall X:Type, paths _ X X) : Type).

[Coq-Club] why Prop appears?, Loic Pottier
- Re: [Coq-Club] why Prop appears?, Adam Chlipala
  - Re: [Coq-Club] why Prop appears?, Alexandre Pilkiewicz