coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Syntax of Typeclasses?

From: Randy Pollack <rpollack AT inf.ed.ac.uk>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] Syntax of Typeclasses?
Date: Mon, 27 Jun 2011 15:48:10 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=PzmLaO03s9bXU4nMWjSsMDNWthKrvmenrnGb4G6GDzYm2X8aUCWFBF+JgJo7SzlS56 BC/FKUcc5xnlVQtASkh9Mhdj0PbTDr5xeUXJat6vAFPkf5bmhKJ3cTXoyZVlB2oS0Ewu YKY+Fp/bDjlIdNsENiSlu1vInzUyBr2LNK7cI=

I'm a newbie using typeclasses in Coq.  I'm using Coq 8.3pl2.
consider the following example from the Reference Man.

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

This is accepted.  I understood from the Manual that I could write

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

but this is rejected: "Error: Unbound and ungeneralizable variable A".

What am I misunderstanding?

Thanks,
Randy

[Coq-Club] Syntax of Typeclasses?, Randy Pollack
- <Possible follow-ups>
- Re: [Coq-Club] Syntax of Typeclasses?, Paolo Herms