coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: A question about "structurally smaller".

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: A question about "structurally smaller".
Date: Tue, 7 Apr 2009 07:27:07 +0200
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 :content-type:content-transfer-encoding; b=szDX+upDaAnXdB3IktgNBhyrWRIFbO74A9ChCTbURpnv7GnsQ/RZjKloRiFhxzxBDo tOrOdUP6kJw6ifh0onxPIVuWdgZYzCBLJlZkeIz+aLOGOjxf/OnH7uqIZ4UCRgJpSRND 4sUOm262chS7hb0+GAqXtqddrgL7caeUVEVZ0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear all,

Sorry about that incomplete message. User intefaces are so powerful
nowadays that by just mistakingly pressing a few random keys you
unwittingly transfer data all over the world. Anyway, composing a more
complete variant of the message let met to solving the problem I was
having all by myself. So no questions from me for the moment, but have
a nice day anyway :-).

All the best,
Chris

2009/4/7 Chris Dams
<chris.dams.nl AT gmail.com>:
> Dear all,
>
> I understand that if I am going to create a recursive function by doing
>
> refine (fix f (l: list A): list A :=
> � match l with
>
> ).
>

[Coq-Club] A question about "structurally smaller"., Chris Dams
- [Coq-Club] Re: A question about "structurally smaller"., Chris Dams