The Coq mailing list

["Jonas B. Jensen" <jobr AT itu.dk>]

It's great to see a tutorial like this done. I hope you will link to
it from the Coq documentation. Here are my comments after skimming it.

- Typos: on page 5, the left unit law is called alternately
"unit_left", "one_left" and "one left".
- On page 6, you write "we consider a class of sort Prop". Then why
not put Monoid in Prop rather than Type when giving its definition?
- In the big example on page 27, should the "=" in the Commutative and
Absorb definitions be "==" instead?
- You reference the paper by Spitters and van der Weegen and follow
most of its design principles in the very last examples. Why not do
that earlier? They seem to be very good ideas.

Cheers,
Jonas

On Wed, May 30, 2012 at 11:36 AM, Pierre Casteran
<pierre.casteran AT labri.fr>
 wrote:
> Hi,
>
> We are pleased to make available a small tutorial on type classes and user
> defined relations in Coq.
>
> It can be found at the following adress
> http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf
>
> The examples (for V8.4-beta) are in
> http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/src-V8.4.tar.gz
>
> Any comments and/or suggestions of corrections are welcome.
>
> Matthieu and Pierre