coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Empty type

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Marco Maggesi <maggesi AT math.unifi.it>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Empty type
Date: Wed, 13 Feb 2013 09:07:52 -0500

On 02/12/2013 01:57 PM, Marco Maggesi wrote:

When I try to define in Coq 8.4 the empty Type but I get an empty Prop.
Is this a bug?

Nope, it's universe polymorphism! :) See the discussion of a very similar example at the end of Section 12.1.1 in CPDT <http://adam.chlipala.net/cpdt/>.

[Coq-Club] Empty type, Marco Maggesi, 02/12/2013
- Re: [Coq-Club] Empty type, Adam Chlipala, 02/13/2013
- Re: [Coq-Club] Empty type, Guillaume Brunerie, 02/13/2013
  - Re: [Coq-Club] Empty type, Guillaume Brunerie, 02/13/2013
    - Re: [Coq-Club] Empty type, Jean-Francois Monin, 02/13/2013
      - Re: [Coq-Club] Empty type, Marco Maggesi, 02/13/2013