coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Function that transforms types
- Date: Fri, 25 Jul 2014 11:36:52 +0200
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
- [Coq-Club] Function that transforms types, Bruno Woltzenlogel Paleo, 07/25/2014
- Re: [Coq-Club] Function that transforms types, Arthur Azevedo de Amorim, 07/25/2014
- Re: [Coq-Club] Function that transforms types, Cedric Auger, 07/25/2014
- Re: [Coq-Club] Function that transforms types, Daniel Schepler, 07/25/2014
Archive powered by MHonArc 2.6.18.