The Coq mailing list

[Chad E Brown <cebrown2323 AT yahoo.com>]

The responses so far provide good answers to question 2, but not question 1.

Why does Coq ignores the explicit ": Type" annotation?

Here is a way to force zero, one and two to be in one of the Type universes.

Is there a simpler way?

Inductive zero : Type := .

Check zero.

===> zero : Prop

Definition zeroT : Type := zero.

Check zeroT.

===> zeroT : Type

- Chad

---

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: Coq-Club <coq-club AT inria.fr>
Sent: Mon, May 2, 2011 9:17:59 AM
Subject: [Coq-Club] void : Type

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