coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] am I cic ?

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Francois.Puitg AT imag.fr
Cc: coq-club AT pauillac.inria.fr, puitg AT imag.fr
Subject: Re: [Coq-Club] am I cic ?
Date: Tue, 16 Nov 2004 12:15:17 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Nov 16, 2004 at 11:37:19AM +0100, Francois Puitg wrote:

> 2) I can't see how typecheck nat  -> Prop with the  Prod rules p.  85.

> T : Type(i)           U : Type(j)
>         T -> U : Type(k)

> Third rule fails since nat : Set and not Type(i).

The CONV rule a few pages after say that if nat : Set, then
nat:Type(i). Hence, this rule applies.

--
Lionel

[Coq-Club] am I cic ?, Francois Puitg
- Re: [Coq-Club] am I cic ?, Lionel Elie Mamane
- Re: [Coq-Club] am I cic ?, casteran