Re: [isabelle] Trying to instantiate a class

I'm afraid Isabelle's type classes are the classical Haskell ones, no extensions. Either do it for lists in general or wrap string in a datatype. Or use a locale instead of a class.


On 25/02/2015 16:42, Andrew Gacek wrote:
I have a class defined as

class foo =
   fixes foo :: 'a

and I am trying to instantiate it over the type "string" but I get an error:

instantiation "string" :: foo
Bad type name: "String.string"

Knowing that string is "char list" I tried that instead, but still got an error:

instantiation "char list" :: foo
Undefined type name: "char list"

Is there any way to instantiate the class over the type "string" like I want?

I know I could try to instantiate at "char" and then do something
general for "list", but it turns out the definitions I want for the
type "char list" are not the same as doing this for char and then
lifting it to lists.

Perhaps I have to wrap "string" in a datatype to get what I want?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.