coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Definitions inside type class definitions (Coq 8.2beta)

From: Brian Aydemir <baydemir AT cis.upenn.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Definitions inside type class definitions (Coq 8.2beta)
Date: Mon, 24 Nov 2008 16:46:54 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

I have another question about type classes in Coq 8.2beta. (-:

When defining a record type, I can use "field_name := foo" in order to
explicitly define a field. Since the type class mechanism is built upon
records (or so it seems), can I do the same when defining a type class?

Simply curious,
Brian

[Coq-Club] Definitions inside type class definitions (Coq 8.2beta), Brian Aydemir
- Re: [Coq-Club] Definitions inside type class definitions (Coq 8.2beta), Matthieu Sozeau
- [Coq-Club] Coq & Java applet, Thery Laurent