coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Purely constructive utility libraries in Coq?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?
Date: Thu, 14 Feb 2019 17:36:51 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f42.google.com
Ironport-phdr: 9a23:+TlEHRetcJmEr+keaVrfDNsmlGMj4u6mDksu8pMizoh2WeGdxcS6YR7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyNOAo2+YIUPAeQPPvtWoZfhqFUBtha+GRCsCfnzxjNUmnP736s32PkhHwHc2wwgGsoDvWnOo9XuKawcTPi1zKjUzTXfcfxWwyz945XPfx86u/2DR6h8cMTLxUk0DwPFj0mQqZD7MDOPzeQAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4wbylfB9SpjwYY1I8W1SEF6Yd64EJtQqjqVO5FqTcMlRmFlvjsxxL4euZOjYiQG1JAqywTcZvGHaYSE/xPuWPuLLTp3mn5ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrnUN2AbS6siDU/d8/kmg1SuW2wDd5exIP1o4laXcK54mzb4wkoQcvV7fES/xnUX6lK6WdkM69ei08+nrfKnqq5uGO4J3igzyKLkil82iDegiPQUCQXCX+eGm273i+U35Tq9KjvozkqTBq5/WP94UqrS3AgNPyYYj8xe/Dyu60NsGh3kHN0lIeB2Cj4fzOlHOJOr0Auu4g1SpiDtr3ezJPqX9ApXRKXjOiKvufbFk60JF1AUzyc1f6IlPB7EaIPPzX1fxu8bCAh84NQy02efnB89n2oMQQ2LcSpOeZYjVqBej4v8la72HY5ZQszLgIdAk4eTvhDk3gwlOU7Ou2M49YWvwJexnP1mUe2Gk1t1HGCEV+BEmTfD2hUeZeTFWbne2Gak742doW8qdEY7fS9X10/S61yChE8gTPzgeUwHeITLTb4yBHsw0RmeXK85lnCYDUOH4GYAk3BCq8gT9zug+d7aGymgjrZvmkeNNyajLjxhrrG57Cs2c1yeGSGQmxjpVFQ9z57h2pAlG8nnG0aV8hKYFR9la5vcMQxhjcJCAlap1DNf9Xg+HddCMGg6r

The corn library has some of the features your looking for:
https://github.com/coq-community/corn

On Thu, Feb 14, 2019 at 5:26 PM Jason -Zhong Sheng- Hu
<fdhzs2010 AT hotmail.com>
wrote:
>
> Hi,
>
> I am wondering is there any purely constructive libraries in Coq out there,
> that can serve as a stdlib alternative?
>
> I am aware of those mathematical libraries that are purely constructive.
> However, those libraries tend to focus on mathematical problems, instead of
> collections, their properties, etc, that are more based on utilities, e.g.,
> Forall, Exists, In, etc that are defined in Type.
>
> Sincerely Yours,
>
> Jason Hu

[Coq-Club] Purely constructive utility libraries in Coq?, Jason -Zhong Sheng- Hu, 02/14/2019
- Re: [Coq-Club] Purely constructive utility libraries in Coq?, Bas Spitters, 02/14/2019
  - Re: [Coq-Club] Purely constructive utility libraries in Coq?, Jason -Zhong Sheng- Hu, 02/15/2019
    - Re: [Coq-Club] Purely constructive utility libraries in Coq?, Abhishek Kr Singh, 02/15/2019
    - Re: [Coq-Club] Purely constructive utility libraries in Coq?, Bas Spitters, 02/15/2019
- Re: [Coq-Club] Purely constructive utility libraries in Coq?, Ralf Jung, 02/26/2019