The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

The use of type classes in lean was somewhat influenced by mathclasses.
(I was at CMU last winter when they were developing this.)

Lean has found a nice way to efficiently implement type classes and
features of canonical structures, but without actually needing to
implement the latter. Jeremy Avigad has worked with in the
math-components team for a year, so he's well aware of the way ssr
does these things.

Their type class implementation also provides some mechanisms for
extending and renaming structures.
It seems light weight, but the repackaging that is done behind the
scenes looks really helpful and natural.
https://leanprover.github.io/tutorial/    (Chapter Structures.)



On Fri, Feb 26, 2016 at 12:01 AM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
> <abhishek.anand.iitg AT gmail.com>
>  wrote:
>> MathClasses has something similar, which I like a lot:
>>
>> http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html
>
> OK, there's a lot of stuff otherwise in MathClasses that I wish would
> make its way into the standard library, too.  I just hadn't noticed
> that one - though it does seem like it could still use more extension
> along the lines I was thinking.  (For example, I see and_dec and
> or_dec there, but no impl_dec.)
> --
> Daniel Schepler