Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] match query

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] match query


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] match query
  • Date: Thu, 05 Jul 2012 15:57:40 -0400

On 07/05/2012 03:36 PM, Terrell, Jeffrey wrote:
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.

The idea of just "returning the function" is ill-typed and more or less nonsensical in Coq, but you could do this:

(**)
Definition f (X : Set) (r : Re X) : { Y : Set & X -> Y } :=
   match r with
      Build_Re _ _ r => existT _ _ r
   end.
(**)

The function [f] returns a slightly more specified dependent record-style package.



Archive powered by MHonArc 2.6.18.

Top of Page