coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dependent return type

From: Santiago Zanella <Santiago.Zanella AT sophia.inria.fr>
To: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] dependent return type
Date: Mon, 15 Jun 2009 10:34:20 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.
(**)

[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