Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Library NOrder

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Library NOrder


Chronological Thread 
  • From: Yves Bertot <Yves.Bertot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Library NOrder
  • Date: Mon, 24 Oct 2016 09:23:05 +0200

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.



Archive powered by MHonArc 2.6.18.

Top of Page