Dear Coq Users,

 

the file Coq.NArith.BinNat contains this definition:

 

Module N

<: NAxiomsSig

<: UsualOrderedTypeFull

<: UsualDecidableTypeFull

<: TotalOrder.

 

I wonder if there is an effective way to define a Module Type with the same interface as the 4 module types given above combined? Just chaining them with <+ like this:

 

Module Type NatInt :=

     NAxioms.NAxiomsSig

  <+ Orders.UsualOrderedTypeFull

  <+ Equalities.UsualDecidableTypeFull

  <+ Orders.TotalOrder.

 

fails, because all of them contain a type t. The only way I see is to include e.g. UsualOrderedTypeFull is to include all its components as shown in this image:

 

 

the colored boxes are module type functors, the white ones module types including a type t. Blue are functions, red are specifications, the darker ones contain definitions/lemmas, the light ones contain parameters/axioms.

 

Is there a smart way of doing this without essentially copying the definition of UsualOrderedTypeFull, UsualDecidableTypeFull and TotalOrder?

 

Should I create Module Type functors matching all the white boxes above?

 

Best regards,

 

Michael