The Coq mailing list

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

Dear Patricia,

 

Starting at PeanoNat bottom up we see:

 

PeanoNat.v imports NProperties.v

 

NPoperties contains this definition:

Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N.

Which aliases the module functor NMaxMinProp as module type functor NBasicProp.

Mixing of modules and module types is possible within certain limits. I didn’t check why this is done in this special case.

 

PeanoNat defines module Nat, which contains

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

This instantiates the module type functor NBasicProp = module functor NMaxMinProp.

 

 

Now starting at NOrderProp top down we see:

 

NOrder defines a module functor NOrderProp.

NOrderProp is included in the module functor NAddOrderProp defined in NAddOrder.v.

NAddOrderProp is included in the module functor NMulOrderProp defined in NMulOrder.v.

NMulOrderProp is included in the module functor NSubProp defined in NSub.

NSubProp is included in many module functors, e.g. NMaxMinProp defined in NMaxMin.v

 

This is the nMaxMinProp included as NBasicProp in module Nat.

 

I once tried to make a tool to automatically create graphical representations of module dependencies, but it is not so easy.

 

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