root edited this page Oct 11, 2017 · 7 revisions
Clone this wiki locally

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.