The Coq mailing list

[Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>]

Hi!

I would like to implement a function that takes a type and returns another 
type.
What I have in mind is something like this:

=====================
(* wrong code below! *)

Parameter i: Type.

Fixpoint f(A: Type) := match A with 
 | (A1 -> A2) => i -> f(A1) -> f(A2)
 | A0 => i -> A0 
end.
======================

I understand why this is wrong (in so many ways!). 

My question is: is it possible at all to achieve this kind of type 
transformation in some other way? If yes, how?

Best regards,

Bruno

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail