The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

Thank you. That's what I was looking for.

Scott Doerrie

Pierre Letouzey 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
> >
> >     
>
> Well, if I remember correctly, the signature FSetInterface.S contains
> a compare function in particular, and others things required in a
> OrderedType, so any instance of this signature can be seen as an
> OrderedType by mere subtyping. This allows in particular to freely
> create sets of sets, or sets of sets of sets, and so on :
>
> Require Import FSets.
> Module NatSet := FSetAVL.Make Nat_as_OT.
> Module NatSetSet := FSetAVL.Make NatSet. (* here NatSet is seen as an 
> OrderedType *)
>
> 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.
>
> Best regards,
> Pierre Letouzey
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>