The Coq mailing list

[Dominique Larchey-Wendling <Dominique.Larchey-Wendling AT loria.fr>]

Vector.to_list ?

Le 20 mai 2020 18:15:53 GMT+02:00, Fritjof Bornebusch <fritjof AT uni-bremen.de> a écrit :

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.

-- 
Envoyé de mon appareil Android avec Courriel K-9 Mail. Veuillez excuser ma brièveté.