The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

Thanks Adam for checking the current trunk. I've been running in the latest 
release.

Thomas Braibant sent a reminder about the containers library which does the 
typeclassification but not the full setoid reasoning. Upon inspection of that 
library, I see I should have written @mem instead of mem. Confirmed in 8.3pl4.

-Ian
----- Original Message -----
From: "Adam Chlipala" 
<adamc AT csail.mit.edu>
To: "J. Ian Johnson" 
<ianj AT ccs.neu.edu>
Cc: "coq-club" 
<coq-club AT inria.fr>
Sent: Friday, July 6, 2012 5:47:37 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Typeclasses and hints?

On 07/06/2012 05:43 PM, J. Ian Johnson wrote:
> I am turning the finite map library into a typeclass and extending it to 
> use setoids. There are different properties about them that are registered 
> as immediate or for resolve, but I can't do that kind of hint registration 
> with typeclass members. For example:
>
> Class TC := { mem : forall x : Type, x = x}.
>
> Hint Immediate mem.
>
> Error: Cannot infer the implicit parameter TC of mem.
> Could not find an instance for "TC".
>    

The above runs without an error for me in Coq 8.4beta2.