coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: Bas Spitters <b.a.w.spitters AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?
Date: Fri, 15 Feb 2019 00:37:44 +0000
Accept-language: en-CA, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BN3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:3hLRPx3mTBiNbrWOsmDT+DRfVm0co7zxezQtwd8ZseMTLPad9pjvdHbS+e9qxAeQG9mDu7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWpPUNhMWSxdDI2ybIUPAOgdMulXtITyvUcCoQekCAWwGO/j1DlFjWL2060g1OQhFBnL0gg6ENIVt3TUqsj+OL4RXuC1y6nIyzrDZO5L1zf99ofIdB8hreiRVrxybMra1E4iFw3YgVWQqI3lJC2Z2vgQv2SH9OdgVeWvi3Iiqw5rozivwt0ghZXOhoIQ013J8zhyzogyJd29UkF7YNikHYNftyGbK4t2Qt4iTHpytCkmzb0GvJi2dzUJxpQ/3xPSZOCLf5KM7x79TuqdPS10iXJmdb6niRa970utxvH5W8Sxy1lFsjZKn9rJu38WyxDe68qKR/5z80i6wzmC1wXe6u9FLE03l6fWLYMqzKQqmZoJq0vDGzf7mEXog6+ScUUp4vCm5vjgbLn6u5OQLpJ5hBnwP6g3ncywGvo3PhIJX2iG5eSzz7rj/VD/QLpXlPE2irPZsJfGJcsFuqG5Hw5V0oEl6xqlCDemzcgYnX0ALFJCexKLlZTmO1bLIPzgDPe/hUqjkCtzyv3JIrHtGJHAImbZnLv9Z7pw601RxBI2zd9F5pJUDr8BIOj0Wk/0rNHYAAI2Mwy1wub8Ftlxyp4SVX6UD6+ZN6PSrVqI6fguI+mIfoMapDH9K/096/70kXA5gUMdfbWu3ZYPdH+4Ge1mL1yFbnron9cOCnwHvhE+TezvkF2NSyRfZ3e0X6Im5zE0EpiqDYnZRtPlvLvU9i6gVqZOZ3xaB0qXWSPiMYzCRLEXcCOOPsJ7iRQLULGgT8kq0hT48EewwL1+a+HQ5ycwtJT51dEz6feZ3UU58iUxBMCA2UmMSXt1lyUGXWll8rp4pBlfw0yE1+A9sfxfE9Mb3PNEVAh/fb7Bh7h0B9DgQViZJ4+hSFG6R9ynBXc6SddnkIxGWFp0B9j31kOL5CGtGbJA0uXTXMVloJKZ5GD4IoNG81iD0aAgi1c8Rc4Wbj+mgbJ6/gnXQYXOlhfAzvr4ReEnxCfIsVy74y+WpkgBC1xwVrnAVHEbIEDRqIahvx6Qf/qVEb0idzB554uCJ69NNoK7q3xjHK6mEvKFJmW7liG3GAqCwa6KYMzyYWIB0S7BCU8C1QcO4XKBMgt4DSCk8TvT

Hi Bas,

do you mind pointing out which folder I should look at? I try to search but the folder structure doesn't look straightforward to interpret.

Sincerely Yours,

Jason Hu

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Bas Spitters <b.a.w.spitters AT gmail.com>
Sent: February 14, 2019 11:36 AM
To: Coq Club
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?

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