Using dot notation with typeclass instsances

Stream: new members

[Kevin Sullivan]

Mario Carneiro said:

If you are using a lemma that takes a typeclass argument in () binders, you will need to specify it. This is sometimes done for typeclasses that are also props and intended to be used as such (i.e. participating in nontrivial logical positions like negations and disjunctions), like nat.prime. It's also necessary to specify typeclasses sometimes when the one that is inferred is not the one you want, which only happens occasionally, mostly when there is a non-defeq diamond in the typeclass hierarchy (which we try to avoid). Plus sometimes it's just the shortest way to write a proof

Thank you, Mario. I also changed the title of this thread to better reflect the subject it addresses.