The Coq mailing list

[Marco Maggesi <maggesi AT math.unifi.it>]

Hi,

I would like to use MSet to manipulate finite sets of strings.  But so
far, I'm lost in the bureaucracy of OrderedTypes and all that.  So I
would be glad if someone can help me with this task.

First question.  It seems that the standard library doesn't provide
yet an order on strings.  So I defined myself an OrderedType for the
strings (see the attached file).  But, despite the fact that the Coq
assures that my module satisfies the necessary signature, when I apply
the functor MSets.MSetAVL.Ops I get the following error that I cannot
track (this arrives at the very end of the attached file)

Error: Signature components for label t do not match: types differ.


Second question: I defined the OrderdType structure on strings in two
steps.  First I defined a module DSO_String with signature
UsualDecStrOrder.  Then I applied the functor DSO_to_OT to it.  Are
there better (i.e. cheaper) ways to obtain an OrderedType?

Thanks,
Marco

Attachment: StringLex.v
Description: Binary data