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.

This article presents an introduction to Coq classes.

See also this article.

Cocorico: TypeClasses (last edited 08-11-2011 03:43:47 by oumix)