coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Purely constructive utility libraries in Coq?
Date: Thu, 14 Feb 2019 16:26:29 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.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 NAM03-BY2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:sPH9TxaAtNmPHElhJCa9QJH/LSx+4OfEezUN459isYplN5qZr8+4bnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrh29qBNy2JTbbJ2JOPdkYq/RYc4WSGxcVchRTSxBBYa8YpMLAeUbJuZYqI/9rEYXoRS9BQmsA+XvyjBVjXHr3a01zeIhEQ7f0Ac9HdwOrWnfodL7NKgPUeC0zbLIwSvfY/9LxTvw84jIchc9ofGJR71wcM7RxVMzGAPCi1WdsIroNC6W2OQVq2WW4PZsWfirhmI5sQ18oyKjy8cyhoXRiIIa1FPJ+Tl8zYswPtK3VFJ0bN2hHZRLqy2XNol7T8YsTm5zoik3yrgLuZC6cSUJypkqwQPUZeadfIiS+B3jUf6cITdmi3Jhf7Kynw68/FSnxOHgWMS4yUtHoShbntXVsXACzALc5tKASvtg4keuwjGP1x3V6u5ZO0w0jbDbK5k9wrEuipUTrUXDHijwmEnsi6+Wa1kk+uyv6+TgYbXqvIOTN4hxig3mM6QunNKwAfggPwUBQ2SX4+Cx2KP58UD4WrlHjuM6nrHcsJ/AJMQboqC5AxVS0oYm8xu/ASqp0NQZnHkcMl5JZA+Lg5TyNlHOJ/D4EfK/jE6tkDdv3fzJIrrhApDVInjZjLjhZap961JbyAcr0d9f4ItUBqgdL/L3R0/+r8fVDgQ5Mgyx2+boEs9x1oIYWWKVA6+WKrnesVGS5rFnH+7ZLoQSoXP2L+Uvz//ol34w31EHN+H91pwOLXu8A/5OIkODYHOqjM1XQkkQuQ9rbuXxj1vKFAxTYHC9F5k86zc0TcqGEM+XSIytkqfbhH7jNp1RemVPC1TKGnDtIdbXE8wQYT6fd5cy2gcPUqKsHtd4hEOe8TTiwr8iFdL6vygRtJbtzt9wvraBlRYu8DV1C4KW1GTfFjgozFNNfCc/2eVEmWI40k2KiPMqg/tEENVS47VCVQJobceBndw/MMj7X0f6RvnMSFuiRYn5UxcYa4pqhvU/OQN6EdjkiQ3f1S23BbNTj6aMGJE/7qPb2T72Otp5zHHFkqImigt/Tw==

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