coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Typeclass tutorial

From: "Perry E. Metzger" <perry AT piermont.com>
To: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Typeclass tutorial
Date: Sun, 6 Aug 2017 20:38:05 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=perry AT piermont.com; spf=Pass smtp.mailfrom=perry AT piermont.com; spf=None smtp.helo=postmaster AT hacklheber.piermont.com
Ironport-phdr: 9a23:aa8wHBLhu6wKeQwLJdmcpTZWNBhigK39O0sv0rFitYgeKvzxwZ3uMQTl6Ol3ixeRBMOAuqIC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJPUMhRSSJPH4CyYIkBD+UOIelWoJLwp0cXrRakGQWgGP/jxz1Oi3Tr3aM6yeMhEQTe0QAuBdwBrm7UrM/1NawPXu651rTDwzLdYPNK2Db955bHcgovrfqRWr9wadTeyVM1FwLFlViQsY3lMC2P1uQItGib6fZgWfizhG4grgF8uz6izdoihInOg4Ia0FHE9SNhzYYoPd23Vkh7Ydi+HJROqi6aKo17Sd4hTWFwoCs217wLtJ+hcCUJx5kr3RzSZ+aaf4WH5B/oSfyfLi1ihH1/fbKynxay/lakyu37TsS00ExFoTZGktnItnACyQfc5dadSvdn5keh2CiA1xrW6uFDJ0A0ibDXJIImwr41jpYTsELDETHqmEjukaObd0Qp9vKr5unoeLnrpIWQO5J7hw3mN6QhgM2/AeA2MggUWGib/Pyx1KX98k3jWrVLjuY7krHYsJ/EP8Qbo6m5AwlJ0oo59xm/CDKm3MwCnXYbNFJFZA6Hj4/xNl7SJ/D4FO6zjEiokDd23P/LJabhA5XILnjbirjtZ7d960hGyAoy199T/ZxUCqtSaM70DwXbudraBxo4NUSfha7fCdhn3Y5UETaFCbeYPbnZvHeD5/lpPvGBYolTtTrgfasL/fnr2DUBlEUHbOGEm9MyZWyqEfl8aQ3NeXf2mMYpCWYHpA85SvCsg1qHB20AL02uVr4xs2loQLmtCp3OE8X02OSM

On Sat, 5 Aug 2017 13:26:47 -0400 "Benjamin C. Pierce"
<bcpierce AT cis.upenn.edu>
wrote:
> Many thanks to everyone who responded to my query a few weeks ago
> about Coq typeclasses. Based on what I learned from that
> discussion (and a bunch of others), I’ve written up a fairly
> extensive tutorial on typeclasses. It can be found here, if you’re
> interested:
>
>
> https://softwarefoundations.cis.upenn.edu/draft/qc-current/Typeclasses.html
> <https://softwarefoundations.cis.upenn.edu/draft/qc-current/Typeclasses.html>
>
> I will probably include it in a future edition of Software
> Foundations, so feedback, corrections, and suggestions for further
> additions are welcome.

Is the source for the .v file from which this was generated available?
It will make it easier to try things out in Proof General.
(I know where the DSSS'17 version is but this seems updated from
that.)

Perry
--
Perry E. Metzger
perry AT piermont.com

[Coq-Club] Typeclass tutorial, Benjamin C. Pierce, 08/05/2017
- Re: [Coq-Club] Typeclass tutorial, Perry E. Metzger, 08/07/2017
  - Re: [Coq-Club] Typeclass tutorial, Yixuan Chen, 08/07/2017
    - Re: [Coq-Club] Typeclass tutorial, Noah Evans, 08/07/2017
  - Re: [Coq-Club] Typeclass tutorial, Richard Ford, 08/07/2017