coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Empty type

From: Marco Maggesi <maggesi AT math.unifi.it>
To: coq-club AT inria.fr
Subject: [Coq-Club] Empty type
Date: Tue, 12 Feb 2013 19:57:39 +0100

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

Welcome to Coq 8.4 (September 2012)

Coq < Inductive empty : Type := .
empty is defined
empty_rect is defined
empty_ind is defined
empty_rec is defined

Coq < Check empty.
empty
: Prop

[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