coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to use GenericMinMax

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to use GenericMinMax
Date: Mon, 24 Oct 2016 13:10:34 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx04.uni-tuebingen.de
Ironport-phdr: 9a23:xDaOwhHZf/1kapIUtu/jK51GYnF86YWxBRYc798ds5kLTJ76r8qwAkXT6L1XgUPTWs2DsrQf2rCQ7f2rAjZIoc7Y9itdINoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScaBx/iwguu14tjYZxhCrDu7e7J7ahus/ivLscxDoo9rN7157QDVr2FNcuJQjTdrIVuOhFD7/du95ptq9SJ4pvQgstJdXK/7eas1S/pUAWJ1YCgO+MT3uEybHkO07XwGXzBOnw==

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

[Coq-Club] How to use GenericMinMax, Klaus Ostermann, 10/24/2016
- Re: [Coq-Club] How to use GenericMinMax, Yves Bertot, 10/24/2016