Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to use GenericMinMax

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to use GenericMinMax


Chronological Thread 
  • From: Yves Bertot <Yves.Bertot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to use GenericMinMax
  • Date: Mon, 24 Oct 2016 13:17:31 +0200

On 10/24/2016 01:10 PM, Klaus Ostermann wrote:
I feel a bit stupid to ask this, but how does one use all the nice Lemmas
(like, say, max_id : max m m = m) in GenericMinMax specialized to the
type "nat"?

Presumably I have to do some kind of functor/module composition, but I
don't
know how and I also can't find any preexisting examples. Or
do they exist in some pre-configured form in the standard library?

Klaus



They exist in some pre-configured form in the library Arith, for instance. Try the following commands:

Require Import Arith.
Locate max_id.

Yves



Archive powered by MHonArc 2.6.18.

Top of Page