coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Library NOrder

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club AT inria.fr
Subject: [Coq-Club] Library NOrder
Date: Thu, 20 Oct 2016 19:02:17 -0300 (UYT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta01.in.vera.com.uy 21B87221BD7
Ironport-phdr: 9a23:/gWhYhaECyYWRBBWAxdodZn/LSx+4OfEezUN459isYplN5qZpc+/bnLW6fgltlLVR4KTs6sC0LuM9f2xEjRcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3p7xirH5o8GbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWdQKT/HoXU2xeqhdSChTZ61muRozpvzHzqvZ68DeXJ8SwRrcxHymzufQ4ACT0gTsKYmZquFrcjdZ92fpW

I want to use proofs from the Library NOrder.

I get the message:

Error: The reference le_0_r was not found
in the current environment.

The same with other proofs.

Is there other library that includes the proofs of NOrder?

Regards

Patricia

[Coq-Club] Library NOrder, Patricia Peratto, 10/21/2016
- Re: [Coq-Club] Library NOrder, Laurent Thery, 10/22/2016
- Re: [Coq-Club] Library NOrder, Yves Bertot, 10/24/2016