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: Clément Pit--Claudel <clement.pit 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 06:57:01 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:jiE9/BaNJZ1o2VWPhGlPsVr/LSx+4OfEezUN459isYplN5qZpci7bnLW6fgltlLVR4KTs6sC0LuK9fy/EjddqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2aufy31vuy+pvcJiwT1GP4OOo6bE/u9USClsAToYZrJqsr5BrEpncAW+lfyW5ybWmYmAz94Mj4vNs+q2UD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWZg8O43YaTlIukwYNRiPB5Qz2U5O55iD+u+9w3jXcJczqZb8xUDWmqaxsTUm72288Kzcl/TSO2YRLh6VBrUf4+kRy

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.

Attachment: signature.asc
Description: OpenPGP digital signature

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