coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dependent return type

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: Santiago Zanella <Santiago.Zanella AT sophia.inria.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] dependent return type
Date: Wed, 17 Jun 2009 10:22:23 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=WXWGjkzGkUPS0+858Nfjy/kNiOhMpLKnJPURMh/k8z+cUVHPaX2rd/PxDwLF1jNUsI uO1q8GazwonN6dhp1MzlVrtSi1zDnlHo59XRgPwYdaw+ByR3WwSQyEGHMZ0GrZWXDXLr rsQ23DBTD4/tk6lCf9F1YolzWUyYJYNqu2rOU=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks Santiago, I had tried to generalize at first, but could not get it to work...
Cheers

On Mon, Jun 15, 2009 at 9:34 AM, Santiago Zanella <Santiago.Zanella AT sophia.inria.fr> wrote:

You can define the same function that Adam suggested interactively. That
way you can avoid writing the generalization of the return type
explicitly.

(**)
Definition F' (t : T i1) : dT' t.
intro t.
unfold dT'.
generalize cast.
case (convertible i1 i2); intro cast'.
apply F.
exact tt.
Defined.
(**)

--
Arthur Azevedo de Amorim

[Coq-Club] dependent return type, Arthur Azevedo de Amorim
- Re: [Coq-Club] dependent return type, Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] dependent return type, Santiago Zanella
  - Re: [Coq-Club] dependent return type, Arthur Azevedo de Amorim