The Coq mailing list

[Jean-Marie Madiot <jmadiot AT CS.Princeton.EDU>]

It says that "A" is unknown. You can provide A as an argument of
negb_impl, as follows:

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

Jean-Marie

On Sat, Jun 11, 2016 at 8:57 AM, Zhaohui Li 
<lizhaohui1991 AT gmail.com>
 wrote:
> 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.
>