The Coq mailing list

[casteran AT labri.fr]

Selon Francois Puitg 
<puitg AT imag.fr>:

Hello,


Type checking of nat -> Prop works using the conversion rule (p. 86).

Since Set <= Type(0)
from nat : Set, you infer nat: Type(0)

Then the 3rd rule of Prop, tells you that
forall (x:nat), Prop  has type Type(0).

The conversion rule explains also your first question.

Pierre




> Hello,
>
> Two questions about the CiC, chapter 4 of the Coq reference manual.
>
> 1) Section 4.1.1 p.  82 tells us that Prop, Set : Type(0), whereas the
> Ax rules of section 4.2 state that Prop : Type(p) and Set : Type(q).
>
> 2) I can't see how typecheck nat  -> Prop with the  Prod rules p.  85.
> Let's simplify them giving up contexts and the global environment, and
> switching to non dependent product. We get :
>
>
> T : s         s belongs to S          U : Prop
> ------------------------------------------------
>               T -> U : Prop
>
>
> T : s         s belongs to {Prop, Set}                U : Set
> ---------------------------------------------------------------
>                       T -> U : Set
>
>
> T : Type(i)           U : Type(j)
> -----------------------------------   with i, j <= k
>         T -> U : Type(k)
>
>
> We  have T = nat and  U = Prop.  First rule  can't  apply since Prop :
> Type, and not Prop.  Second rule neither because Prop  : Type  and not
> Set. Third rule fails since nat : Set and not Type(i).
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.