coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dealing with equalities in dependent types

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr, Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
Subject: Re: [Coq-Club] Dealing with equalities in dependent types
Date: Sat, 21 Jan 2017 10:37:26 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f51.google.com
Ironport-phdr: 9a23:cZU+LBzcirmnHHvXCy+O+j09IxM/srCxBDY+r6Qd0e4WIJqq85mqBkHD//Il1AaPBtSHra4ZwLKL++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Dq3PF4XTl8W60fyps92WOl0QxWn1XbQnJxKv6A7Vq8M+gI14K693xAGN6lhMcvlNjURzOV+Jmh/64I/k/5pq7j8WvOk9+tRFWKP8V7k+TPlEETksMmY66cutuRSVHiWV4X5JbGwakx8AMQHB7Q/zFsPvoCL+t/R08CKfIIv7Qa1iCmfq1LtiVBK90HRPDDU+6myCz5Uo1K8=

On Fri, Jan 20, 2017 at 3:44 PM, Emilio Jesús Gallego Arias <e+coq-club AT x80.org> wrote:

Others will disagree, but in my opinion Coq's vector library is not
suitable for extended use.

If you working with vectors, I recommend CoLoR (http://color.inria.fr/) VectUtil module as a nice extension of Coq vector library. It offers "an extensive library on vectors including many basic functions and theorems on vector manipulation, vector product/lexicographic ordering, vector arithmetic, vector components filtering and permutation"

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] Dealing with equalities in dependent types, Klaus Ostermann, 01/20/2017
- Re: [Coq-Club] Dealing with equalities in dependent types, Dominique Larchey-Wendling, 01/20/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Anton Trunov, 01/20/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Klaus Ostermann, 01/20/2017
- Re: [Coq-Club] Dealing with equalities in dependent types, Emilio Jesús Gallego Arias, 01/20/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Anton Trunov, 01/20/2017
    - Re: [Coq-Club] Dealing with equalities in dependent types, Emilio Jesús Gallego Arias, 01/21/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Vadim Zaliva, 01/21/2017