coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with dependent match statement
- Date: Fri, 15 Sep 2017 22:03:48 +0000
- Accept-language: en-GB, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jeffrey.terrell AT kcl.ac.uk; spf=Pass smtp.mailfrom=jeffrey.terrell AT kcl.ac.uk; spf=Pass smtp.helo=postmaster AT EUR01-DB5-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:G6bxYhc9Yt3EcQun3d1SdZselGMj4u6mDksu8pMizoh2WeGdxc2ybR7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpW1aJhKqfwFyP6H+HpPYp8WxzeG7vZPJKU0cjz2kJLh2MR+erAPLt8BQj5E0eYgrzR6c6EdFYf5bwWcsbXCekRjm69b6tMph/ipeof8wsdJNS7/3e6AQTrdcSj0tdX02sp64/SLfRBeCsyNPGl4dlQBFVlDI
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
Hello Michael,
Could you clarify what you mean by your last sentence.
I came across the tabulate function in an Agda tutorial, and wondered what it
would look like in Coq.
tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f fzero :: tabulate (f o fsuc)
In the last line, f is of type Fin (suc n) -> A without qualification.
Regards,
Jeff.
> On 15 Sep 2017, at 12:29, Soegtrop, Michael
> <michael.soegtrop AT intel.com>
> wrote:
>
> Dear Dominique, Jeff,
>
> yes, sorry for my stupid comments. I knew the usages of Fin as type for
> index parameters for functions with a vector parameter (as e.g. standard
> library nth), but I didn't see the usefulness of such a type in a function
> which actually creates a vector. I guess in
>
> Fixpoint tabulate (n : nat) (A : Set) (f : Fin n -> A) : Vec A n :=
>
> it is known that A is a set with n elements so that f can't be defined for
> a different parameter type.
>
> Best regards,
>
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0,
> https://emea01.safelinks.protection.outlook.com/?url=www.intel.de&data=01%7C01%7Cjeffrey.terrell%40kcl.ac.uk%7Cd965375b45f84bccf8ec08d4fc2d264f%7C8370cf1416f34c16b83c724071654356%7C0&sdata=7JMEfzPqM1RaK9J9Ef1ijKqoWIJVeS6X2BLaPb%2BNRFU%3D&reserved=0
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
- [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/15/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Jan-Oliver Kaiser, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Dominique Larchey-Wendling, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/15/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Dominique Larchey-Wendling, 09/15/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/16/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/18/2017
- Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/21/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/22/2017
- Re: [Coq-Club] Problem with dependent match statement, Terrell, Jeffrey, 09/16/2017
- RE: [Coq-Club] Problem with dependent match statement, Soegtrop, Michael, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Dominique Larchey-Wendling, 09/15/2017
- Re: [Coq-Club] Problem with dependent match statement, Dominique Larchey-Wendling, 09/15/2017
Archive powered by MHonArc 2.6.18.