coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] type conversion

From: "Lucian M. Patcas" <lucs12 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] type conversion
Date: Fri, 27 Aug 2010 20:29:22 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=PbLjiMZZ7stB4H+wa4LuBlz5+xNak8dD2SAWDBttSqKozCbU5aeoRJnqfSbx0iYNN0 4Db+ss+w6rObyAWczJeH7CLCk0tYgfaUGcj18fFb0N+gQkSnQdd+8tJqAUtV4TbudXIW rdwlSxr5NrTbolZnpxS40ORRW8oNNle1c1FIY=

Hello,

In the standard library, prod is defined as:

Inductive prod (A B : Type) : Type := pair : A -> B -> A * B

I have tried something like

forall t : nat, prod t bool

and the typechecker complained that t was not of type "Type". But t : nat : Set : Type. Unless I am missing something, how can I convince the typechecker to do this type conversion?

Thanks,
Lucian

[Coq-Club] type conversion, Lucian M. Patcas
- Re: [Coq-Club] type conversion, Taral