The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 2 May 2011 02:34:53 -0700 (PDT),
Chad E Brown 
<cebrown2323 AT yahoo.com>
 a écrit :

> 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

I didn't know that this trick could work;
another way (but not quite the same) is:

Definition T := Type.
Inductive zero : T := .

(then if you unfold T in the terms containing it, you will retrieve
Type and not Prop); i didn't expected it to work either
(I expected it to be parsed and accepted, but then cast to Prop).

But for me, this is not an important question, as I see no case where
you specifically want a Type and not a Prop as a Prop works everywhere
a Type works (the only bad point I see is when you want to destruct
something which is a Prop to produce a Type, but as I wrote earlier,
coq manages it well and allows such a destructuration in that
particular case).

The only cons of this behaviour I see are:
* the behaviour is disturbing (but, that is not the most disturbing
  point in Coq {see the "x is of type T while it is expected to be
  of type T", where some implicit parameters occur in T})
* acceptation of applications of functions "Prop -> Type" to "zero"
  where you may want it to be refused (but does it really happens?)

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