The Coq mailing list

[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
> 
>