coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Standard library not listed?
- Date: Mon, 24 Dec 2018 13:43:19 +1100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f48.google.com
- Ironport-phdr: 9a23:qcYX/BO/70ax1LGE1Nsl6mtUPXoX/o7sNwtQ0KIMzox0Iv39rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYosKEuoBPvhXr5L9p1ATsRu+BAetC/n1yj9Jm3T72qg60/kiEQ7YxwwgH84OsHXardrvLqcSUPq5zKjJzTXCc/NW3Czw6IfNch87oPGMWah8ftbWyUkqDg7IiEibp4LiPzOQzOsNsm6b4vJhVeKpkW4nqht+riKhxsc2koXJiYMVykzE9SVk24k5P8G3SEl+YdK8H5tQtj2aN4trQsw5WW1kojo1yroDuZO9YSMEy4wnygbBZ/Cbd4WE+BHuWeaLLTtlmn5oe6izihmx/EWm1+byTNO70ExQoSpAitTMtm4C1xjU6sWfT/ty5Eah2TKW2wHd7+FIPFk4laTUJpMi2LIwmZ0TsUPMHi/yhkr6lrOZdkIh+uSw6uTnZKvppoOEOoNqlg3zNr4il8+/DOgiLwQCQWuW9f6z2bDg5UH5Ra9FjvwykqnXqpDaIsEbq7a8Aw9I0YYs9Q2/Dze60NQZk3gINkhFeBOdg4joOlHOIez4DfKkjlSjlTdk3fHGPrn7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S/F7IEiCYTLwg8gIC2ZC6g8jT+HxiEGDTjdJZjCzXqMg4xk0DYunCcHIQYX70+/J5zuyApADPjMOMVuLC3q9L9zVCcdJUzqbJ4paqhJBULGgT4E70hT37V31zrNmKqzf/ShK7Mu/hugw3PXakFQJzRIxF96UijjfQGR9n2dOTDgzjvgm/B5Nj2yb2K09uMR2UNxe4/QTD1U/PJ/YivN/UpX8BlKHcdCOR1KrBN6hBGNpQw==
Hi Cao,
Coq maintainers could give the answer more precisely, but based on my understanding standard library [1] lists theories [2], while the library (setoid_ring) you are looking for is in plugins directory [3]. If I am looking for documentation that is in plugin directory then I do a Google search (name of directory/file in plugin directory + coq ), but you can construct the url by yourself using the directory name (setoid_ring) with the coq file (Ring.v) (https://coq.inria.fr/library/Coq.setoid_ring.Ring.html). Hope it helps.
Best,
Mukesh Tiwari
On Mon, Dec 24, 2018 at 10:23 AM Cao Qinxiang <caoqinxiang AT gmail.com> wrote:
Hi all,I am wondering whether there are some standard library folders missing on the page "https://coq.inria.fr/library/index.html". For example, I cannot find setoid_ring on it. I am wondering where I can find a more complete list of standard libraries. Thank you very much!Best,Qinxiang CaoShanghai Jiao Tong University, John Hopcroft CenterRoom 1110-2, SJTUSE Building800 Dongchuan Road, Shanghai, China, 200240
- [Coq-Club] Standard library not listed?, Cao Qinxiang, 12/24/2018
- Re: [Coq-Club] Standard library not listed?, mukesh tiwari, 12/24/2018
- Re: [Coq-Club] Standard library not listed?, Cao Qinxiang, 12/24/2018
- Re: [Coq-Club] Standard library not listed?, mukesh tiwari, 12/24/2018
Archive powered by MHonArc 2.6.18.