The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

I'm trying to make an OrderedType(WithLeibniz) so that I can make an
MSetList. However, I'd like to write as few proof as possible, and the
ways I've found seem to require more proofs than I'd have thought were
necessary.

I've found Coq.Structures.OrderedTypeEx, but it doesn't seem to make
something of the right type, e.g. eq_equiv and lt_strorder are missing.

I've also found
    http://permalink.gmane.org/gmane.science.mathematics.logic.coq.club/7252
which looks like it is meant to be a working example, but when I try it
the proofs for eq_equiv and lt_strorder are missing.

Has anyone got an example of the best way to make an OrderedType, e.g.
for nat, please?

I have coq 8.4pl3 (December 2013).


Thanks
Ian