The Coq mailing list

[Marco Maggesi <marco.maggesi AT gmail.com>]

Oh, I see.  I should have read the manual more carefully.

Thank you Adam, Guillaume and Jean-Francois for your quick responses.

Marco

2013/2/13 Jean-Francois Monin 
<jean-francois.monin AT imag.fr>:
> Indeed:
>
> Inductive em: Set := .
> Check em.
> em
>      : Set
>
> JF
>
> On Wed, Feb 13, 2013 at 09:12:38AM -0500, Guillaume Brunerie wrote:
>> >> […] More precisely, an empty or small singleton inductive definition is 
>> >> set in Prop, a small non-singleton inductive family is set in Set, and 
>> >> otherwise in the Type hierarchy.
>> >
>> > Guillaume
>> >
>> > On 2013/2/12 Marco Maggesi 
>> > <maggesi AT math.unifi.it>
>> >  wrote:
>> >> 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
>>
>>