The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 24 nov. 08 à 22:46, Brian Aydemir a écrit :

> Hi,

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?

Not yet, in 8.2 you don't even get to parse that.
It is parsed now (in current trunk), as we completely unified parsing of
record/class/(co-)inductive declarations but not supported in
instance declarations (thanks for the accidental bug report :). Of  
course
the question is, do you get the right to redefine it afterwards à la  
Haskell.
Currently it works like for records, creating a let-in in the  
constructor, with
no redefinition allowed.

Cheers,
-- Matthieu