coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Typeclass tutorial

From: Yixuan Chen <xlk AT umich.edu>
To: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Typeclass tutorial
Date: Mon, 7 Aug 2017 20:46:16 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xlk AT umich.edu; spf=Pass smtp.mailfrom=xlk AT umich.edu; spf=None smtp.helo=postmaster AT mail-pf0-f194.google.com
Ironport-phdr: 9a23:nAT4ShyxyAmdt+DXCy+O+j09IxM/srCxBDY+r6Qd2+gfIJqq85mqBkHD//Il1AaPBtSLraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CS2RPXthfWS9DDYOycoUAAPYOMP1CoIXhvVYDtweyCRWuCe7p1zRGhmX23ao/0+k5Ew7G3QMhH88Uv3TSsd74KqcSXv6zzKLVyjjCYPdW2TTm5YjVdxAhoO2DXbJqfcXP1EYvChrIg1ONooLrODOV0/4Cs2md7+d4WuOvj20npxt0ojex3sssl5HJiZwTylDC7yl23ps6JcC+RUVmYtCkCINduz+GO4ZyWM8vQGFltDwnxrACp5K3ZjUGxZAoyhLHdfCLb5aE7gj+WOqPPTt0nm9pdbalixqv/kWtxOvxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw/kK71jaO0wDf8/lEIU4omabCJZ4t37o9m5UJvUTMGS/2n0r2jKuIeUk+5ueo7OHnbq3npp+aKYB0lhnzProylsG7G+g1MQgDU3KG9em4yrHv51D1TbFFg/Eul6nWqpHaJcAVpq6jBA9V154u6hm7Dzely9kYgHwHLFNZdxKHlYTmJUzBIO3gAfeln1usiCtrx+zBPrD5HprNKWHDnK79crZ59k5T0xE+zctf5pJRErEOOuj/Wk73tNzCDx82KRa4w+j9CIY16oRLE0iCBK2QNaLU+XTOrtouLvOHacVd7Dz2M/ko/fXjpXQ4ghkAZaSv290aZG3uWrxtJFzcan7xiP8AF30Lt0wwVr/EklqHBA9Sd2u7WeoX5jw9QNa2CYTrW4Wsi7zH0SumSM4FLltaA0yBRC+7P76PXO0BPWfLepds

Hi, I found that the source file is just available if you change the suffix from html to v.

Luke Chen
Email: xlk AT umich.edu
Education: UMJI SJTU / Univeristy of Michigan
Homepage: https://blog.xlk.me

On Aug 7, 2017, 8:39 AM +0800, Perry E. Metzger <perry AT piermont.com>, wrote:

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