[isabelle] Trying to instantiate a class

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?


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