The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jean-Marie,

wasn't the meaning of the back quote that all unbound variables shall be 
implicitly generalized? It looks like a bug to me.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jean-Marie Madiot
Sent: Saturday, June 11, 2016 3:14 PM
To: Coq Club 
<coq-club AT inria.fr>
Subject: Re: [Coq-Club] Question about examples of TypeClass in 
reference-manual

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.
>
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928