coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MhonArc 2.6.16.