coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] nth element of a vector

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] nth element of a vector
Date: Wed, 20 May 2020 17:15:33 +0200
Authentication-results: mail3-smtp-sop.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:F7XK4RTq+EGzJ2W944S/cI8Kxtpsv+yvbD5Q0YIujvd0So/mwa6ybRSN2/xhgRfzUJnB7Loc0qyK6v2mADRRqsba+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLq8UanY9vJqkyxxbHv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqRJ/zYDKfY+bN/Vxcb/Act4BWWpNQtxcWzBdDo+gbYYCCfcKM+ZCr4n6olsDtRuwBROtBOPzyD9IgXH21rAn3uQmCwHG2hIvEMkTsHTPsNr1NLoZXOe7zKnSzDXDc/FW2TDz6IXTbxAhp/CMUatrfsrL10YvEh3KjlOKpYP4ITyYz+IAuHWU4OR8T+ygkXInqx1vrTi1wMchkorEip4Jxl3K9Ch0xIY4KNy8RUJmf9OpH5teuSGaOoZrRs4sTGJltDs6xLAEt5O2eDQHxpspyRPea/GKcoiG7BzlWe2MLzl4g3dld6i+hxa06UWgy+v8VtO10FlQtCZFnMPMu3YQ3BLQ8siKUuZx80mu1DqVygzf9v9ILVo0mKbHMZIt37w9moIQvEjdBCP6hln6ga2Mekk65OSk9v7rb7Xmq5KaKoR6kBvxMr40lcy6Gek4MhYBX2yc+emk273s51b2QK9LjvIolqnVqY7aJcECqqKnGQNU04gj6xClAze71tQYnGALI0lfeB2ZiojmJVfOLOrlAvihm1iskTFryO7aPrD5H5nAIHfOnK38cbph9UJQ0go+wcxF655JCLwNOPfzVVXwtNzcAB85KQu0w+P/BdVzzIMeWH6PAq2eMKPcqlKI++QvI+iVaIAOojbyNf0l6ODojXMjhFASY7Gl3YELZ3CgAvRmP0KZbGLwjdcGCGcGpxYxTOj3iFKZSjNTfHazX6ck5j4hEo6mDIHDRpqsgLObxiu7EIdWNSh6DQWHFm6tfIGZUd8NbjiTK4lviG8qT7+kHqE71A2sswGy4b19KOfe5zYTtdq32sJ0++/Umzkv8z0xBd6Q1myLCW15yDBbDwQq1bxy9BQugmyI1rJ11qQBSI5joshRWwJ/Dqbyiux3D9epAFDOd92TSVuiB8ujRGt3XNw3hcIIYgN3AdingxaF0yf4W+ZExYzOP4Q99+fn51a0Is98z3jc06x40gs7RMoKP3erg6N5sQTeVdeQzxep0p2yfKFZ5xbjsX+ZxDPT7lxeUUt6S6jAUHZZakaE9dk=

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