The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

I have difficulties to understand the structure of the Orders standard library. I thought the idea is that Orders.v contains definitions of structures as module types, and that OrdersFacts contains module functors which help instantiating modules of these types by providing lemmas and proves.

 

But OrdersFacts also contains module types, many of them with lemma definitions in them. E.g. why is OrderedTypeFacts a module functor, but OrderedTypeFullFacts a module type functor? Other module types which a naïve user would think should be modules are CompareFacts, CompareBaseOrderFacts and BoolOrderFacts. Maybe I could make better use of the standard library, if I would understand the logic behind such decisions.

 

Thanks & best regards,

 

Michael