Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] am I cic ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] am I cic ?


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page