coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Typeclass tutorial

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Typeclass tutorial
Date: Sat, 5 Aug 2017 13:26:47 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT hound.seas.upenn.edu
Ironport-phdr: 9a23:P5pPoRxquVmNANjXCy+O+j09IxM/srCxBDY+r6Qd1OIRIJqq85mqBkHD//Il1AaPBtSLraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolCgIODA3/nzUhMJui6xWuwiuqwB6w4POYIGZKPhzc6XAdt0aX2pBWcNRWjRPDo6hcYQPCegBMvxdr4n8oVsFsAWzCROxD+31yz9HmGX20rEk3OgvDArL2xcvEM4WsHTVstr1LrsdXv6uwabUzDXDdOla2Srl6IfWdBAhp+uAUqxtfsrM0EQiER7OgFuXqYzgJTyV1+INvnCG7+p4S+2vjWgnpxtvrTey28chjJTCiIENyl3c6Cl0wIU4KcelREN1fdKoCplduzyAO4drTM4uX3lktSc0x7Ecp5K3YioHxI4lyhPdcfCLbYiF7g/lWe2MOzl3nmhld6i6hxuq8Uiv1On8Vs6s3VZKqSpFj9/MuW0X2xzI9MeIUOB98l282TaXyQ/T7OdELVoqmqXGNp4t2r8wlpwNvkTfBiL6hUX7gayMekk59OWk9/7rb7f7qpOGKoN5hB3yPrwrmsOlAOQ4NgYOX3Kc+eS5zLDs5lH2QK1LjvIoiKnWrI7VKN8Hqa64GA9ZyJsj6w6hADeg1tQUh2cII09YeB6flYjmJ0nOIOzkDfe4m1mjjDBrx+nfMrL9BpXNM2PMnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tNzCXVcFNFm/xP+iA9Fg3KsfX3iOC+mXKvD8q1iNs6gFLu+ObYoUvn7WbbAd5vP0hnJz0QsXdrGo0IEcZVizH+8gPl2UZ3yqj9scRzRZ9jEiRfDn3QXRGQVYYGy/Cvox

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

I will probably include it in a future edition of Software Foundations, so feedback, corrections, and suggestions for further additions are welcome.

Best,

- Benjamin

[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