coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] nth element of a vector

From: Tadeusz Litak <tadeusz.litak AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] nth element of a vector
Date: Sat, 23 May 2020 03:48:17 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tadeusz.litak AT gmail.com; spf=Pass smtp.mailfrom=tadeusz.litak AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f48.google.com
Ironport-phdr: 9a23:tYQ4ZBHJuloyd59RZ4elnJ1GYnF86YWxBRYc798ds5kLTJ7yp8WwAkXT6L1XgUPTWs2DsrQY0reQ6vm8EjBfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmssAndq8YbjYRtJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWoAi8qRJhzY7aYIKbOvRwcazSf9wVWWVPU91NVyFDGI6wc5cDAuQDMOtesoLzp0EOrRy7BQS0Gu3g0CJHiWHr3a0h0uUqDAfI3A08H90Us3TfsdL4NLsIXu+o0qbI0C7DbvJM1Tf56YjIbgouofKXULJ/dMre00gvFwffglqMrozlOiqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hh4fVi4wV11zJ6Cp0zZopKNC7VkN1Yd2pHZlSuiyUKYd7QMAvTW5mtig0xbMLtpy2cTUIxZonxxPTd+GLfoeL7x/lSe2fLzB4hHd/d7K+gRa/6UmgyuvmVsm1yllGtCRFksPKu3sQ1BLT8tCKRuVh8kqlwzqC1ADe5vtZLUwqlqfXMZEsz70ompYOv0nPAzX6lFj1gaKVbEkp+/Kk5/n5brjgu5SSLZV7ihvkPaQrgsG/Afo3MgwJX2WD/OSzzrzj/UngTLREi/06j7DVsJ7VKMkYvKK5DAhV0oEs6xa7ETiqysgXnX4CLF5deRKHiZbmO03WLfzmEfuyh06gnTRryvzcI7HtHJbAImLMnbriZbp97lRTyAs3zdBR/ZJUDbQBLervWkDrqdPXEAI5Mxe1wur9DNV9158eVniMAqKCP6PStEWH5uMrI+WWeIAVvzP9J+A/5/HylX85hUMdfa6x0JQLb3C4B+1qLFmdYXrxmdgMCnwKvwo7TOzyklKOSz9TZ3CoX6I9/D43EoymDZ2QDryq1beGxWKwGoBcTmFAEFGFV3nyJL+JQ/MdVCXHPsZtnyEfR/6lSpMo1jmhsQb7z/xsKe+H1DcfsMff3dR4+vbB3TUz6TV3R5CB2m2AUnpm2GcJWzY19K96qE15jFyE1P4r0LRjCdVP6qYRAU8BPpnGwrkiUoGgakf6Zt6MDW2ebJCjCDA1QMg2xoZXMUl4EtSmyBvE2njzWuJHp/mwHJUxt5nk8T3xKsJ6kSuU0aAgixw5R5IKOzH2wKF48AfXCsjClEDLz//2J5RZ5zbE8SK49UTLpFtRCVciXqDMXHRZbUzT/4z0

Hi Fritjof,

this discussion has been going on for a few days already and it seems that nobody has suggested to use ssreflect vectors (n.-tuple) instead.

In my limited experience, this has so far proved the most usable solution. All the other ones sooner or later seem destined to brutally remind one of idiosyncrasies of dependent pattern matching in Coq.

In particular, the function you're looking for seems directly available.

Do you have important reasons to stick with Coq.Vectors.Vector?

Best,
t.

On 20.05.20 17:15, Fritjof Bornebusch wrote:

Hi there,

I'm looking for a function that iterates over a vector -
https://coq.inria.fr/library/Coq.Vectors.Vector.html - and returns
the Zth element, like the nth element of a list.

The library function only dealy with the Fin.t type, but I need Z.
Does anyone has a suggestion or hint?

Best Regards,
--f.

[Coq-Club] nth element of a vector, (continued)
- [Coq-Club] nth element of a vector, Fritjof Bornebusch, 05/20/2020
  - Re: [Coq-Club] nth element of a vector, Agnishom Chattopadhyay, 05/20/2020
    - Re: [Coq-Club] nth element of a vector, Fritjof Bornebusch, 05/20/2020
      - Re: [Coq-Club] nth element of a vector, Clément Pit-Claudel, 05/20/2020
  - Re: [Coq-Club] nth element of a vector, Dominique Larchey-Wendling, 05/20/2020
    - Re: [Coq-Club] nth element of a vector, Fritjof Bornebusch, 05/20/2020
      - Re: [Coq-Club] nth element of a vector, Talia Ringer, 05/20/2020
        
        Re: [Coq-Club] nth element of a vector, Fritjof Bornebusch, 05/21/2020
      - Re: [Coq-Club] nth element of a vector, Dominique Larchey-Wendling, 05/20/2020
        
        Re: [Coq-Club] nth element of a vector, Fritjof Bornebusch, 05/21/2020
  - Re: [Coq-Club] nth element of a vector, Tadeusz Litak, 05/23/2020
  - Re: [Coq-Club] nth element of a vector, Frédéric Blanqui, 05/23/2020