Skip to Content.
Sympa Menu

coq-club - [Coq-Club] match query

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] match query


Chronological Thread 
  • From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] match query
  • Date: Thu, 5 Jul 2012 19:36:27 +0000
  • Accept-language: en-GB, en-US

Hi,

Consider

Inductive Re : Set -> Type :=
   Build_Re : forall X : Set, forall Y : Set, (X -> Y) -> Re X.

Given an inhabitant of Re X, is it possible to return the function argument that was used to construct it? I can see why the following doesn't work but I'm not sure how to fix it.

Definition f (X : Set) (r : Re X) :=
   match r with
      Build_Re X Y r => r
   end.

Thanks.

Regards,
Jeff.



Archive powered by MHonArc 2.6.18.

Top of Page