coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] nth element of a vector

From: Fritjof Bornebusch <fritjof.bornebusch AT dfki.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] nth element of a vector
Date: Wed, 20 May 2020 16:54:48 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof.bornebusch AT dfki.de; spf=Pass smtp.mailfrom=fritjof.bornebusch AT dfki.de; spf=None smtp.helo=postmaster AT lnv-91185.sb.dfki.de
Ironport-phdr: 9a23:m4UNbhVq0EbIMOzgzy18ZuamzmPV8LGtZVwlr6E/grcLSJyIuqrYbB2Ot8tkgFKBZ4jH8fUM07OQ7/m9HzVYsN3e4DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrNQajZdmJ6o+yBbEoWZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJxw4DafpybOvlxcazBYNwXXnZBUtpLWiBdHo+wc4kCAuwcNuhYtYn9oF4OoAO+Cwm2BePv1j1Ihnj43aYnzukhFhvG3Ao+EN0VrXTUt8n6NKcPWu2ywqnI1zTDb+9U2Tf65ojEaAsuofaWXbJ2b8Xe0lQvFxjZgVWQsoHqIj2V1ucMs2SB8uVvS/uihmg6oA5+vjah3N0jipXVho0L0FDE8z10zJo6KNC5R0N2f9+pHZRUuiyaKYZ7TN0uT3x0tCs6xbMLuJ62cicXxJkj2xPRZfOJfoqK7x7+SeqdPTR1inxrdb+5mh28/0+gyujmWcm11lZHtitFkt/WtnAMzRPf8MaHSuF780y82jiPzxje5vxKLE07j6bWL58szqQtmpcXrEjPBDL6lUb2gaOOdUgo5PKk5/r7brjkvJOQKZF4hhzkPqkumsGyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07iq3ZsJbEJcgCoqO1HhJZ34Uj5hqlFDepy84UkmQJLFJGeRKLlZXmNE/WLPD5C/ewnUisnS92y/3IMbDtGJHAI3nZnLv8ebtx9lRQxBcwwN1f/55UD6sOIPP3Wk//rtzYCRo5PhS6w+b9CdV9yoEeWWWBAqODK6zStkWI5uQxLOaXeY8VoyryK/g+6vHzg385ml4dcbO00pQJcHy4BOhpI12FYXrwhdcMCXsFvg0nTODzlFKCVSNTaG2pUqIn5jA7DZqmAp3ZSoCshryBxia7EYdMamBIEFDfWUvvIo6DQrIHbD+YCs5niD0NE7a7GKE70hT7mhX717hgIKL+/TceuJj+z9N1r7ndjxAu9zt6Sc6ayWeARXxvlWMgSzE13eZzrBoumR+4zaFkjqkARpRo7PRTX1JibM+O/6lBE9n3Hzn5UJKMQVeiTM+hBGBjQtwywpkCbhQkQojwvlX4xyOvRoQtufmLCZgzqPiO237vYpckkiabkrIryVUoQcoJOWD03vcjpTiWPJbAlgCir4jvbb4VjXzB+mSCi2aD7hlV

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