Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?

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: 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.



Archive powered by MHonArc 2.6.18.

Top of Page