coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Extracting several elements of a tuple at once

From: Roman Beslik <beroal AT ukr.net>
To: Eduardo Ochs <eduardoochs AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Extracting several elements of a tuple at once
Date: Sun, 02 Aug 2009 14:28:29 +0300
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I suggest you to try "match ... with (a, b, c, d, e, f, g) => ... end".

Eduardo Ochs wrote:

Hello list,

this is probably a basic question (I'm a newbie) but anyway, here it
goes... If abcdefg is a 7-uple - with a complex dependent type - is
there a way to extract all its components at once? Something like this
would be ideal,

Definition (a, b, c, d, e, f, g) := abcdefg.

but this is not accepted...

--
Best regards,
Roman Beslik.

[Coq-Club] Extracting several elements of a tuple at once, Eduardo Ochs
- Re: [Coq-Club] Extracting several elements of a tuple at once, Laurent Th�ry
- Re: [Coq-Club] Extracting several elements of a tuple at once, Roman Beslik