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:14:34 +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:2nv0HRxs3CXu1hbXCy+O+j09IxM/srCxBDY+r6Qd2+MSIJqq85mqBkHD//Il1AaPAdyGrasc2qGH7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhDexe65+IAmyoAnessQbgZZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8J+jKxVvg+vqR9xw4HbfI6aKfhxc7jBfd8GX2dNQtpdWzBDD466coABD/ABPeFdr4Tlp1UOtxq+BRWuBOPoxD9Dm2L73aog0+QnDw7JxxEgH8kSv3TUsd74M6kSUfq0zKnUzzXDaP1W1Czg6IjOcxAtuOqDXahufsrU10YvERnJgUiOpoH8OT6ey+sCvXSB4eV6SeKvl3Aoqxt3ojW3yckglIbHip4bx13Z6yh13Jg4KcGlREN7f9KqH5pdujyVOYdqXs8vQ2JltDg+x7AHpJO2eCcHxpsnyhPRdvGKfY6F6Q/tWuaWJDd3nnNleLSnihaz90ig0Oz8WdOu3FZEtCpIlMTHuHMV1xHL98SKRPRw8l281TqTyQzf8OFJLVwumabGKZMt2r09moQJvUjdAiP7ml/6gLGIekk54OSl6+Tqb7P7rZGGLYB0kBvxMqE2l8y/H+s4Ng8OUnCU+eumz7Lj50z5T6tOjvEvjKnZtYnWKdoBqq+4DQ9V1Jwv6wu5DzenydgXhmMHI0xAeB2ZiYjlIUzBL+7gAfe+hVSjjitryujbMrDvDZjBNGXPnKv/cbpn60NQ1BA/wc1d6p5MD7EOOvPzWkv/tNzCCR85NhS5w+j9CNV8yoMeW2WPAqGCPaPPt1+I5/sjLPKWZIALvTbyNf4l6+TzgnAngVMdZ7Wm3YMLaHCkGfRrO1mWYX31gtsYDWgKuhc+Q/fxhV2ZUT9TYm6yULgm6jE6DoKmF4bDSZq3jLyPxifoVqFRM2tBExWHFWriX4SCQfYFLiyIceF7lTlRe6KgV40m21mEsxX8xrB6NeHUsnkWr5P/1t97z/DVlFQ47zFxAsLb32zbHDI8pX8BWzJjhPM3mkd60FrWifEp0cwdLsRa4rZyail/MJfdy+JgDNWrB1DceNbMQkyrR9igRz08HItono0+Jn1lEtDntSjtmiqnB7hOze6EDZYu86/Ymmb0Ypw72XjAkrQnjhwsWMZKOGvgiqMtr1GPVb6MqF2QkuORTYpZxDTErTrR0GyP+UtCXQt9V+PJUCJHaw==

This function requires a Fin.t type, but I have Z as "index" type:
Definition nth {A} :=
fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=

On Wed, May 20, 2020 at 10:20:25AM -0500, Agnishom Chattopadhyay wrote:
> I see a function called `nth` over here:
> [1]https://coq.inria.fr/library/Coq.Vectors.VectorDef.html
> Does that work?
>
> On Wed, May 20, 2020 at 10:15 AM Fritjof Bornebusch
> <[2]fritjof AT uni-bremen.de> wrote:
>
> Hi there,
> I'm looking for a function that iterates over a vector -
> [3]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.
>
> References
>
> 1. https://coq.inria.fr/library/Coq.Vectors.VectorDef.html
> 2. mailto:fritjof AT uni-bremen.de
> 3. https://coq.inria.fr/library/Coq.Vectors.Vector.html

[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