coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
Jeff.
- [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.