Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "Core" Coq typeclasses

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Core" Coq typeclasses


Chronological Thread 
  • From: "John Wiegley" <johnw AT newartisans.com>
  • To: Daniel Schepler <dschepler AT gmail.com>
  • Cc: Coq Club <coq-club AT inria.fr>, "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
  • Subject: Re: [Coq-Club] "Core" Coq typeclasses
  • Date: Mon, 19 Jun 2017 17:51:38 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg0-f65.google.com
  • Ironport-phdr: 9a23:j/numR/7btR+gf9uRHKM819IXTAuvvDOBiVQ1KB30O8cTK2v8tzYMVDF4r011RmSDNqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RfQ8heVSJPAoS/YYsBAeUOMvpXopLhp1cStxayGRWgCfnzxjJOm3T43bc60+MkEQze0gAuG9UOsHTSrN7oNKgSUP66zKbMzTrdb/Ja1yr25Y/KchAmofGMW7xxfNHXyUYxGQLKlE+QqZDkPzOOzOsNtXOb4/B8WuKojm4qsgd8qSWhyMcrj4nGnIMVylbc+CV/3ok0K8e3SFRnYd6lC5tfrSeaN5BsTsw+RGFovSA3waAFt56jZCUHypsqywTCZ/CZc4WE+BHuWeiLLTp5hH9pYLCyiheo/US+xODxWdO43VdOoyZfj9XBuXQA2hrO4cadUPR95F2u2TOX2gDT9O5EJUc0mLLeK5E7w74wkoMfsVzMHiPqgUn2gq6be0U+9uin7OTnZbrmppuCOINulg7+NaEultS+AeQ+LAcOQ3CW9Oaz2bH54EH1XrVHguc1n6TXqpzXJMQWqra8AwBP04Yj7xi/Dy2h0NQdhXQHLlxEeBOZgIjmP1HBPvD5AOywg1SpijhrxvTGMqf9DZXKK3jPiK3hcqpl605A1AozyshS6I5TCrEYOf78RkvxtMHDARIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhAlD/7KvUhr8XljXIhnVIHNf2lxpAXZWi8E+5OLECQYH6qidAERzQkpA07GabIj12EGQFSanm2UrN2rmU5D4KgEq/FS5+kmqCAxy69BdtdYWUQWQPEKmvha4jRA6REUymVOMI012VcDbU=
  • Organization: New Artisans LLC
>>>>> "DS" == Daniel Schepler
>>>>> <dschepler AT gmail.com>
>>>>> writes:

SD> More generally than EquivDec, I often end up adding a "Decision"
SD> typeclass:

It might be nice in the stdlib to generalize this and other patterns. For
example, we have a [reflect] data type that could become a type class, so one
only has to remember one function to convert between (n =? m = true) and n =
m, no matter if you're using Z or N or nat or positive, etc. I find myself
frequently searching for the same pattern, just at different types.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

Archive powered by MHonArc 2.6.18.

Top of Page