coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Map facts and properties
- Date: Fri, 10 Nov 2017 01:44:48 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=arthur.aa AT gmail.com; spf=Pass smtp.mailfrom=arthur.aa AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot0-f173.google.com
- Ironport-phdr: 9a23:d4u2RBDFsJJxjNk7bUUhUyQJP3N1i/DPJgcQr6AfoPdwSP77p8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6lX71zMZGw3+OAxpPay1X9eK14Xkn9y1rrbUek1jgCe3Ked5KwzzpgHMvOEXh5FjI+A/0E2ajGFPfrF/339oOEjbtgTx+Mq8+9Zv/mx5vvU79ssIBazgY6QlV/pRBRwpNmk04IvgshyVHljH3WcVTmhDykkAOAPC9hyvG86p6iY=
Why are the WFacts and WProperties modules defined separately in Coq.FSets.FMapFacts? Given that they are parameterized by modules of the same types, wouldn't it be simpler to just merge them?
- [Coq-Club] Map facts and properties, Arthur Azevedo de Amorim, 11/10/2017
Archive powered by MHonArc 2.6.18.