coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. |
- [Coq-Club] match query, Terrell, Jeffrey, 07/05/2012
- Re: [Coq-Club] match query, Adam Chlipala, 07/05/2012
- Re: [Coq-Club] match query, Paolo Herms, 07/05/2012
Archive powered by MHonArc 2.6.18.