The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

On Wed, Nov 26, 2008 at 5:38 PM, Pierre Letouzey
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> On Tue, Nov 25, 2008 at 02:56:21PM -0500, M. Scott Doerrie wrote:
>> I've been searching the Coq standard library and have been unable to
>> find a functor that creates an OrderedType given an FSet or even a List
>> of OrderedTypes.  This seems relatively straightforward given the
>> implementation of PairOrderedType, so I've probably missed it.  I'd
>> rather not duplicate effort, so I thought I'd ask first.
>>
>> Scott Doerrie
>>
> Concerning lists of OrderedType.t, FSetList.Make is building a
> FSetInterface.S whose base type is a sorted list attached with its
> sortedness proof. As before, this FSetInterface.S can be seen as an
> OrderedType. If you want to deal with arbitrary lists and not only the
> sorted ones, nothing exists yet in the standard library, but it should
> not be too difficult to build something (indeed, PairOrderedType can
> be a good source of inspiration). If you write this kind of functor,
> let me know, it might be interesting to include it in the standard
> library.

I had actually written such a functor (see attached file) some time
ago, it builds an ordered type for lists with pointwise equality and
lexicographic order. [eq] and [lt] are defined as inductives rather
than functions because I find inversion really convenient.

Hope this helps,

Stéphane L.


-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

Attachment: ListOrderedType.v
Description: Binary data