The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

You can find a formalisation of ordered types like Coq.Structures.Orders but 
using type classes in the Containers user contribution library :
http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.3
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France


On Friday 04 November 2011 13:25:12 Victor Porton wrote:
> Coq.Structures.Orders uses module types.
> 
> It is advised to not use module types at
> http://coq.inria.fr/cocorico/RecordsNotModules
> 
> My question: Should we start to build on Coq.Structures.Orders or first
> rewrite it from scratch?
> 
> I studied a reasonably big subset of Coq and my now attempt to start writing
> formalizing mathematics, if it will happen that I will find time.
> 
> Should I first rewrite Coq.Structures.Orders?