The Coq mailing list

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

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

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

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