coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Sort hierarchy

From: Bas Spitters <spitters AT cs.ru.nl>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Sort hierarchy
Date: Tue, 12 Jan 2010 13:18:18 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=MEA/RnVkNtwnrJPV8Gy33K9zl1+fqqAzjvI2lBHBvrVIcEAUHVVP1Xpu7uFMUPDzRU dg5ib+56V4ydX9BbjUBmMWRADkhv23jGyTvhHfsMEBeKOai2hbKR31J2W14KhRT0FKuj +gj4DKgnRRqgbN+zAbO7LOQDU5luJbJ6TPeNo=

I recently learned that the Coq sort hierarchy has changed. Prop is
now a subsort of Set.

Could anyone tell me about the reasons for this change and its
theoretical motivations?

Thanks,

Bas

[Coq-Club] Sort hierarchy, Bas Spitters
- Re: [Coq-Club] Sort hierarchy, Hugo Herbelin
  - Re: [Coq-Club] Sort hierarchy, Bas Spitters
    - Re: [Coq-Club] Sort hierarchy, Hugo Herbelin