The Coq mailing list

[Yves Bertot <Yves.Bertot AT inria.fr>]

On 10/21/2016 12:02 AM, Patricia Peratto wrote:

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

File NOrder.v contains a functor, not a module.  A functor is like a function, it only creates its output when given enough intputs.  Here, it needs an input module to generate an output module.  In this case, what it needs is a module describing a type of numbers that have the basic properties of natural numbers.  The module it produces contains the theorems you want.  This is useful machinery to share the same proofs about arithmetic for several implementations of the basic numbers.  But the theorems produced by the functor only exist when the function is actually applied to some input.


Laurent Thery already suggested to require module PeanoNat which performs this functor application (among others).  I was going to suggest loading a more comprehensive module, like Arith or NArith.

Require Import Arith.

Locate le_0_r.