coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. |
- [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
Archive powered by MHonArc 2.6.18.