coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] libraries for setoids?

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] libraries for setoids?
Date: Mon, 1 Oct 2018 00:15:01 +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 NAM04-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Lh9BwxYpvI9SuSJJ+yvVe/H/LSx+4OfEezUN459isYplN5qZr8++bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrh29qBNy2JTbbJ2JOPdkYq/RYc4WSGxcVchRTSxBBYa8YpMLAeUbJuZYqI/9rEYXoRS9BQmsA+XvyjBVjXHr3a01zeIhEQ7f0Ac9HdwOrWnfodL7NKgPUeC0zbLIwSvfY/9LxTvw84jIchc9ofGJR71wcM7RxVMzGAPCi1WdsIroNC6W2OQVq2WW4PZsWfirhmI5sQ19vySjyt0sh4TNno4VxE7L+CZlzIswINC3Ukp2bcC/H5ZVqi2XNZB5Qs0nTmxrpik10bgLtJ+gcygE05sqwQPUZeadfIiS+B3jUf6cITdmi3Jhf7Kynw68/FSnxOHgWcS4yUhHoDNYntXVsXACzALc5tKASvtg4keuwjGP1x3V6u5ZO0w0jbDbK5k9wrEuipUTrUXDHijwmEnsi6+Wa1kk+uyv6+TgYbXqvIOTN4hxig3mM6QunNKwAfggPwUBQ2SX4+Cx2KP58UHkXLlGlP07n63BvJDfP8sbp6q5AwFP0oYk7hayFzmm38kYnXgGN1JJZg6Lg5X1N1zVIPD4Cuu/g1G2nzdqw/DKJKHuApLILnTbirfuYa5961JAyAo01d1Q+5VUCqgYLP3vXk/xqcfXAwQiMw20xubnEM9y2pkfWWKJGK+ZMbndvUWG5uI1cKGwY9pfszHkbvMh+vTGjHkjmFZbc7Pjlc8cb2n9FfB7KW2YZ2Dti5EPCzFZkBA5SbnIgUaFV3YWVXa1Wa103TE2Do3jRafeDtSjjLyTx33jR8V+ZmdaD1mNFTHjcIDSCKREUz6bPsI0ym9MbrOmUYJ0jUj/5j+/8KJuK6/vwgNdsJvi0NZv4OiKzkMy8iBxBsWZlWqKSjMtxz9ad3oNxKl65HdF5BKby6Eh2K5YEsBW7vJNFAw9MMyElrEoO5XJQgvEO+yxZhOmT9GhXW5jaPsUm4NLSGEkXtKog1bEwjagBKITm/qTHpso/6nA3n/3YcFg13LB06pnhF4jEJJC

Hi all,

I am wondering are there any libraries which fully commit to setoids in Coq? I am looking for ones that push the idea of setoids as far as possible. For example, agda's standard library (agda-stdlib) is entirely built around setoids. I am mainly looking for libraries that handle list and relations around it in that manner and hoping someone has done some work.

Sincerely Yours,

Jason Hu

[Coq-Club] libraries for setoids?, Jason -Zhong Sheng- Hu, 10/01/2018
- Re: [Coq-Club] libraries for setoids?, John Wiegley, 10/03/2018
  - Re: [Coq-Club] libraries for setoids?, Bas Spitters, 10/03/2018