coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] nth element of a vector
Date: Wed, 20 May 2020 18:15:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT gabriel-vm-2.zfn.uni-bremen.de
Ironport-phdr: 9a23:mqwdPRx4ekNOPgjXCy+O+j09IxM/srCxBDY+r6Qd2+MQIJqq85mqBkHD//Il1AaPAdyGrasc2qGH7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhDexe65+IAmyoAnessQbgZZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8J+jKxVvg+vqR9xw4HbfI6aKfVwcaHGcNMGRmdMRNpdWzBdDo6+aYYEEuoPPfxfr4n4v1YArQG+BQiwBOPtzT9IiGL90LA90+Q7FwHJwhcvH88VsHvIrNX+KaAfUe6vzKnJ0TXDbfRW2Tnm5YjVdBAhoOiAUqlqccXPzEkgCQXFgk+NpoP7Jj6Y0PkGvGeH4eR6T+2vl3InpB9rojip3sohhYnEipwIx13A+yh0wIg7KcO5RUB7YtOpDpteujyeOoV2TM4sTWFltDomx7AbpJO2fCgExZYnyRPdb/GJc4yF7xT+X+ifJjd4gWhqeLO5hxuq8EigzPf8Vsiu31pQoCpFiN/BvW0O2RzL8sWLV/Vw80i71TqSywzf9PtILEAomabBNpIswKY8m5kNvUjZACP6hEf7gLWIekk65+Sk8eTqb7Xgq5SBLYF7kBv+Pb4rmsGnAeQ3LAwOX2+D9OSzzrLs5lf5QLRUgf0yi6XZrpXaKd0FqqKjAg5V3IAj5wyiDzeg0dQUhGIILEhbdxKCkYfpPUvCL+3mAvunglSslilkx+zeM7H8DJjAIWLPnKr9cbpj8UJRyBY/wcpC659WEr0BJej8Wk71tNzWFB85NAm0zv7pCNVn14MeRWCPAqiXMK7JrF+I4OMvL/CXa48Ppjn9LuYq5/j0gXAkh1ARZbOp0ocPaHCkAvRmJF2UbmbrgtcYCGsFog4+TPHxh1CZSj5SZ3OyX7om6T0hCYKmC53DRoG3j7Cb0ie7BM4eWmcTAVeVVHzsao+sWvEWaSvULNUyvCYDUO2PUY491xag/CX90bxqJPfP8S1Q4Zz51cR34OP7iBczsDZuAsGQ1SeBQjcnzSszWzYq0fUn8gRGwVCZ3P0g2qAKJZlo//pMFzwCG9vE1eUjVoLvXAOEdM2ETVugBNmrU2loE4ABhuQWakM4IO2MyxDO2y3xWe0anraRBZEwt7zZmiK3Nch7jWvA1ewrlVQjT80JOWD03vcupTiWPJbAlgCir4jvcK0d2CDX82LakDiTukAdWhR9VKjDG3wSNBLb

On Wed, May 20, 2020 at 05:29:19PM +0200, Dominique Larchey-Wendling wrote:
> Quick fix ... project your vector into a list ;-)
>

Interessting, do you know any function that does that for me?

>
> ----- Mail original -----
> > De: "Fritjof Bornebusch" <fritjof AT uni-bremen.de>
> > À: "coq-club" <coq-club AT inria.fr>
> > Envoyé: Mercredi 20 Mai 2020 17:15:33
> > Objet: [Coq-Club] nth element of a vector
>
> > 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, Fritjof Bornebusch, 05/20/2020
- <Possible follow-up(s)>
- [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