The Coq mailing list

[Victor Porton <porton AT narod.ru>]

02.11.2011, 02:16, "Jelle Herold" 
<jelle AT defekt.nl>:

> šOn Nov 1, 2011, at 10:38 PM, Victor Porton wrote:
>> ššWhat is the difference between type classes and dependent records?
> šI'm am by no means an expert, but I'm pretty sure they will join this 
> discussion soon enough to correct my mistakes :)

http://coq.inria.fr/cocorico/TypeClasses :

When you define a type class using Class, all of its members will be declared 
such that the argument for the instance is implicit. If you would prefer that 
this were not the case, simply use Structure instead. They are identical 
except for this one difference.

And in Coq reference it is said:

Structure is a synonym of the keyword Record.

Thus the only difference is presence of implicit arguments. Right? What 
experts can say?

--
Victor Porton - http://portonvictor.org