coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?
Date: Sun, 22 Jan 2017 15:12:21 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f53.google.com
Ironport-phdr: 9a23:fJ5VnRxntIcvyPrXCy+O+j09IxM/srCxBDY+r6Qd0u0XIJqq85mqBkHD//Il1AaPBtSHra4bwLWL++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9dazJHdvZiN3y3OSv8bXSZR9JjXyze+BcNhKz+CfYrc4QyaR4Lb0qgk/Lq2BPfetMwnhzdHqcmh/94oG7+5s1oHcYgO4o68MVCfayRK8/V7ENVDk=

You dropped the ": Prop", which, I believe, makes it not land in Prop. If you don't drop it, you get an error message saying that universe variables can't be instantiated with Prop, if you do that.

On Sun, Jan 22, 2017, 6:57 AM Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

On 2017-01-21 13:59, Jason Gross wrote:
> Definition natP : Prop.
> Proof.
> let v := (eval compute in (bar nat)) in exact v.
> Defined.

You can write this as "Definition natP := Eval compute in bar nat.", I think :)

Clément.

Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, (continued)