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] 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 LemmasThey exist in some pre-configured form in the library Arith, for instance. Try the following commands:
(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
Require Import Arith.
Locate max_id.
Yves
- [Coq-Club] How to use GenericMinMax, Klaus Ostermann, 10/24/2016
- Re: [Coq-Club] How to use GenericMinMax, Yves Bertot, 10/24/2016
Archive powered by MHonArc 2.6.18.