The Coq mailing list

[Zhaohui Li <lizhaohui1991 AT gmail.com>]

Dear all,

I follow examples of TypeClass (Chapter 20) in reference manual,

and enter this code:

Class EqDec (A : Type) :=
  {
    eqb : A -> A -> bool ;
    eqb_leibniz : forall x y, eqb x y = true -> x = y
  }.

Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).

But it throws an error at the last line:
Error: Unbound and ungeneralizable variable A

I try Set Implicit Arguments, but it doesn't work.

My coq version is 8.5.

Thanks for help.