The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Actually, the let construction can do the job. For example:

Definition f (x: nat) := (x, x, x).

Eval compute in

  let '(x, y, z) := f 1 in

    (x, y, z).

Pay attention to the single quote character after the let keyword. This let sintax is explained in the session "Second destructuring let syntax" of the Coq reference manual (https://coq.inria.fr/refman/Reference-Manual004.html)

Regards,

Saulo

On Sat, Aug 6, 2016 at 6:08 PM, Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> wrote:

You can use match, or if you want to use let it seems you have to do it in 2 stages:

let (p, c) := f x in let (a, b) := p in ...

In fact this is what Coq prints if you do

Check (fun x => match f x with ( (a,b),  c) => 0 end).

Gaëtan Gilbert

On 06/08/2016 23:00, Aymeric Fromherz wrote:

Hi,

I have a function f with signature nat -> nat * Z * Z

I would like to retrieve the result values when calling it by doing
let (a, b, c) := f n,
but I get the following error :
Error: Destructing let on this type expects 2 variables.

Is there a way to do something similar?

Thanks,
Aymeric Fromherz