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?

From: Jason Gross <jasongross9 AT gmail.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, 01 Jul 2016 19:58:48 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f48.google.com
Ironport-phdr: 9a23:f2+qXBH6XEUG3NoWAsIgLp1GYnF86YWxBRYc798ds5kLTJ75osiwAkXT6L1XgUPTWs2DsrQf2rKQ6vGrADddqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxjrH5osaOKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t37Yv/F63mG1J8rtVvhgWz256KFkUhjzk3YvODsw8WWRgct12vEI6Cm9rgByltaHKLqeM+BzK/vQ

Not sure if this went through before (it seems like the image put it above the size limit?)

I'm not sure if there's a way to combine two modules with a common element, you should be able to (ab)use the fact that modules and functors are duck-typed to not rewrite any proofs; modules that instantiate your module types (as long as they have all of the right names with the right types that match the standard library exactly) should also by typeable as the standard library modules.

RE: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?, Soegtrop, Michael, 07/01/2016
- Re: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?, Jason Gross, 07/01/2016