The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Inductive zero : Type := .
Check zero.
===> zero : Prop

Inductive one : Type := O : one.
Check one.
===> one : Prop

Inductive two : Type := A : two | B : two.
Check two.
===> two : Set

1. Why does Coq ignore my wish to place the types
in one of the universes Type ranges over?

2. Why are zero and one put into Prop while
two is put into Set?

-- Gert