Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Function that transforms types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Function that transforms types


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




Archive powered by MHonArc 2.6.18.

Top of Page