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.
- 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
Archive powered by MHonArc 2.6.18.