[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