coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Returning a tuple from a function

From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Returning a tuple from a function
Date: Sat, 6 Aug 2016 23:08:21 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Pass smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:VI9VahQILil78PU2w+vQ1rpnQtpsv+yvbD5Q0YIujvd0So/mwa64YBSN2/xhgRfzUJnB7Loc0qyN4vimCTJLuM3b+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0q8OYOl4SzBOGIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1QVX3kflFJnAgzP4QvmFsP+uybmv+w71yieN8DsUZg5Xy/n67ZsTlnmknFUZHYC7GjLh5ko3+pgqxW7qkknzg==

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

[Coq-Club] Returning a tuple from a function, Aymeric Fromherz, 08/06/2016
- Re: [Coq-Club] Returning a tuple from a function, Gaetan Gilbert, 08/06/2016
  - Re: [Coq-Club] Returning a tuple from a function, Saulo Araujo, 08/06/2016