coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] nth element of a vector
Date: Wed, 20 May 2020 12:24:00 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f48.google.com
Ironport-phdr: 9a23:SETsExM2AoePi80Zn7Il6mtUPXoX/o7sNwtQ0KIMzox0I/z6rarrMEGX3/hxlliBBdydt6sZzbOO4uuxBCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagYb5+Ngi6oRnVu8UZhYZvKrs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxGvhyhqRxxzY3abo6bO/VxfL/Sc9wBSGpdXMtcTTBNDp+yYoYNCecKIOZWr5P6p1sLtRazGw2sA/nqyjBWgH/2wbU13f4gEQHaxQAtAdYOv27JrNroKqgSVf2+wa7UwjXbbvNWxSvy6IzSfRA8vP6DQ7ZwfNHeyUkqDQzFj1GQpZb5MDOS0+QAqm6W5PdvWuyzkWAosR1xoiSxycc2jInEnp4Zx1TK+yt33Yo4JNK1RU1nbNO4H5ZdqyGXOoh5TM4/Q29luSI3xqAGtJOlYCUHx5QqyhzbZvGZcIWG7RPuWeKXLDxlh3xlYKqyiwiu/UWk0OHxVcm53ExUoiZYltTArH8A2h/L5sSZS/Zx4lqt1DOS2w3Q5exJJE85mbfYJpI9x7M9l5sevlrBEyLzg0r5kbWZe0Uh9+ey9+vqYqnpq5qBO4BplA7yLqEjlde+DOk6MAUDWXWQ9/6m273550L5Ra1Hjv0onandt5DXPcEbqbS4Aw9Ry4oj8gi/Ayq/3NQWknQKL0hJeB2Aj4juNFHOJO73Ae2jjFSrlTdn3/HGPrv/DZXRNnXPjqvtcLJn50NfyAc/185T649QB70bL//+WVf9tNnCAR84Nwy0zfznCNJ41o4GRW2PGq6ZML/Ovl+M/O0vPvSDa5ERuDvmJPgl4uThjX49mVMHYaap2p4XZGiiHvt6O0WZfWbsgtAZHGgWuQo+VfXmh0GGUT5OfHm/RLk85zE+CIK+F4jPXIGtgLqb3Ce6BJJafG5GCkrfWUvvIo6DQrIHbD+YCs5niD0NE7a7GKE70hT7nwt7zrdhMt3s+zFdnpbqydR446WHngkz6TdwBtmR3mWlQGR9n2dOTDgzivMs6Xdhw0uOhPAry8dTEsZesqsQD1UKcKXExuk/MOjcHwLMetDTFQSjS9SiRCgvF5c/n49IbEF6FNGvyBvE2njyWuNHp/mwHJUxt5nk8T3pPc8kkiTJ0aAgix8tRc4dbTT31J46zBDaAsvyq2vckq+rcaoG2yuUrTWMyGOPuAdTVwsiCKg=

On 20/05/2020 12.14, Fritjof Bornebusch wrote:
> 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 :=

Just cast your Z to nat, then to a Fin.t?

[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