coq-club AT inria.fr

Subject: The Coq mailing list

List archive

chronological Thread

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Typeclasses and type abbreviations, anyone?
Date: Wed, 3 Feb 2010 15:06:40 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=ZtTwWove/fCw3w/vqc/OIxKRjmx2ae+PqXNbyFcwb41SuJjMuagI+YTw+HO8AgL/EA xdhrUz/uMNYzo0Dy76AwTalbGKVyujZH6EAhe5UBPI1AR1j/UWKzRECbIQvLLxK3xPoq 1nZp2DydbhFm3cx53A0EODh/c8yJVPx0DfW2Y=

(*�Hello list

�*

�* �Ok, this seems like a really silly problem... Let's take an EqDec class as defined in the manual:�

�*)

Class EqDec (A : Type) := {

�eqb : A -> A -> bool;

�eqb_leibniz : forall x y, eqb x y = true -> x = y

Section test.

��Variable A : Type.

��(* here, everything works as expected *)

��Definition test `{w : EqDec A} (a b : A) :=�eqb a b.

��(* but if we introduce a type abbreviation: *)

��Definition eqdecA := EqDec A.

��(* then this doesn't work:

> Definition test' `{w : eqdecA} (a b : A) :=�eqb a b.

�� I also tried it with:

> Typeclasses Transparent eqdecA.

�� and with replacing Definition with Let in [eqdecA]; both to no avail.

�� *)

End test.

(*�I'm using 8.2pl1; what am I missing?

�* Best, Adam

�*)

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[15 rue Berlier, 75013 Paris, France]
Sent from Amsterdam, NH, Netherlands

[Coq-Club] Typeclasses and type abbreviations, anyone?, Adam Koprowski
- Re: [Coq-Club] Typeclasses and type abbreviations, anyone?, Matthieu . Sozeau