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:

[cid:image001.png@01D1D2F8.57A8D5E0]

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
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928