coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Mandy Martino <tesleft AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] how to search these rules in Ring library?
Date: Sun, 7 Feb 2016 01:45:47 +0000
Accept-language: en-US, zh-HK
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT BLU004-OMC1S24.hotmail.com
Ironport-phdr: 9a23:01l7JRFJ3zjDJd/mqDNq551GYnF86YWxBRYc798ds5kLTJ75ocywAkXT6L1XgUPTWs2DsrQf27WQ6fyrADxQqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0ocGYOlUYzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePFyRrtBST8iLmod5cvxtBCFQxHFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63Xy/NMv6XPgRUC6+7qFsAEv0hTwDOjAl2GHQlsl5jaYdqxWk8U8si7XIaZ2YYaItNpjWeskXEDJM

Hi ,

i can import Ring library, but find no this link in https://coq.inria.fr/library/

coq.inria.fr

The Coq Proof Assistant. The Coq Standard Library. Here is a short description of the Coq standard library, which is distributed with the system.

Require Import Ring.

SearchRewrite Reflexivity.

SearchRewrite Transitive.

SearchRewrite Symmetric.

Regards,

Martin

[Coq-Club] how to search these rules in Ring library?, Mandy Martino, 02/07/2016