[Coq-Club] Returning a tuple from a function

[Aymeric Fromherz]

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

[Gaetan Gilbert]

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

Post by Aymeric Fromherz
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,
Error: Destructing let on this type expects 2 variables.
Is there a way to do something similar?
Thanks,
Aymeric Fromherz

[Saulo Araujo]

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

You can use match, or if you want to use let it seems you have to do it in
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

Post by Aymeric Fromherz
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,
Error: Destructing let on this type expects 2 variables.
Is there a way to do something similar?
Thanks,
Aymeric Fromherz