coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Returning a tuple from a function

From: "Aymeric Fromherz" <aymeric.fromherz AT ens.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Returning a tuple from a function
Date: Sat, 6 Aug 2016 23:00:39 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=aymeric.fromherz AT ens.fr; spf=Pass smtp.mailfrom=aymeric.fromherz AT ens.fr; spf=None smtp.helo=postmaster AT nef2.ens.fr
Importance: Normal
Ironport-phdr: 9a23:naKLfBa2eWvX+la7SrFldxb/LSx+4OfEezUN459isYplN5qZpci7bnLW6fgltlLVR4KTs6sC0LuO9fC+EjVbu96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JXvkbDssMSIOU1hv3mUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF7Fz2oZX38XmVJmGQ/A7BzgTN255iLrs+dn2SLcM9fxSLA5QyaK4qFwDhHy3nRUfwUl+X3a35QjxJlQpwis8kRy

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