coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction]

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction]
Date: Sun, 17 Dec 2017 17:21:20 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:Ac3AMRdKaDJIJr06GUN/JcIQlGMj4u6mDksu8pMizoh2WeGdxcu+YR7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyxPDJ2hYYsIAeoPM+RXoYrzqFQBsRSwChKhBP/2yjJSmnP6wbc33uYnHArb3AIgBdUOsHHModrrL6oTXuO4wLXSwTXEdfNW1ir25IzHfBAkoPGMWbNwcc3MwkcrCQzFlU+IqZf4ND2UzOsNt2yb4PRvVeKolmUqtxtxojm1ycc3j4XEgJ8exFPc9Shh3Yo4Jt61RFRlbdK6EZZcrTyWOolrTs84Xm1ltjg2xqUFtJO6ZiQHyZYqywTbZvCdboSE/hDuWeCMKjlinn1lYqiwhxOq/Eig1OL8Us603U5FrydGjtXArHcN1wbc6sSfS/t9+Fmu2SqX2gzO6exJIlo4mbTFJ5Mg2LI8i5gevVnZEiPrlkj6kreadkA+9eip7+TnbK/mppiZN4JslA7zKasvl8+jDegiNQgORWeb9fym1LL/5U35XKlKjvoun6bFt5DaPN0XqbK9Aw9IyYku8A2/Djej0NQAh3YLNlNFeBSdj4joIV7COv74De3sy2irxR5nzvWOFb3lA43EKnGLxL7tdLN2w0VHwQs3i9Ve+9RZBqxXc9zpXUqkufTIXkd/NBa7i6bKDdR514RWe2+UkLTRH6rWtVKH4aoGOeiFf85G637GN/E56qu23jcCklgHcPzshMNPZQ==
Organization: X80 Heavy Industries

e AT x80.org
(Emilio Jesús Gallego Arias) writes:

> What should then the proper alternative recommended alternative for
> sized lists in the standard library?

I meant:

What should then the proper recommended alternative be?
[In particular in the context of Coq's standard library]

E.

[Coq-Club] Trouble with dependent induction, Matěj Grabovský, 12/17/2017
- Re: [Coq-Club] Trouble with dependent induction, Jasper Hugunin, 12/17/2017
  - Re: [Coq-Club] Trouble with dependent induction, Adam Chlipala, 12/17/2017
    - [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Emilio Jesús Gallego Arias, 12/17/2017
      - Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Adam Chlipala, 12/17/2017
        
        Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Robby Findler, 12/17/2017
        
        Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Emilio Jesús Gallego Arias, 12/17/2017
        
        Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Emilio Jesús Gallego Arias, 12/17/2017
        
        Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Xavier Leroy, 12/17/2017
        Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Emilio Jesús Gallego Arias, 12/20/2017
        
        Re: [Coq-Club] Vector in Coq [Was: Re: Trouble with dependent induction], Adam Chlipala, 12/18/2017
    - Re: [Coq-Club] Trouble with dependent induction, Matthieu Sozeau, 12/17/2017
      - Re: [Coq-Club] Trouble with dependent induction, Matěj Grabovský, 12/19/2017