coq-club AT inria.fr
Subject: The Coq mailing list
List archive
RE: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?
Chronological Thread
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?
- Date: Fri, 1 Jul 2016 14:55:26 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
- Ironport-phdr: 9a23:L3h4fBQZI4HF7ETmOXWaDQc5aNpsv+yvbD5Q0YIujvd0So/mwa64YhGN2/xhgRfzUJnB7Loc0qyN4vimAD1Lv8bJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mj6brqtaNM01hv3mUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG679ZuEzSaFSJDUgKWE8osPx/1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6v/NF61SaGJ8ruCfgRWD+i5qpvAle8jSYMNzc09CfMjcF/kLhcuDqgoQByx8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUWo4=
Dear Coq Users,
just before I rewrite half of the standard library (I just made variants of Equalities, Orders, GenericMinMax and NZAxioms where all module types get the base type as parameter), can someone confirm that there is no way to combine two module types with a common element (say a type t) into one bigger module type (see the example below)?
In case this is not possible: how do you live with the structure module types as defined in the standard library? Is there a good reason why was the standard library is done like this, that is it for some reason a bad idea to give every module type a type parameter (and maybe some others)?
Best regards,
Michael
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr]
On Behalf Of Soegtrop, Michael
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 Intel Deutschland GmbH |
- RE: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?, Soegtrop, Michael, 07/01/2016
Archive powered by MHonArc 2.6.18.