Re: [isabelle] Trying to instantiate a class
You can instantiate a type class only for a type constructor such as "list", not for
compound types such as "char list". Since "string" is a type synonym of "char list", the
type class instantiation for "string" must match the instantiation for "char list". If
"char list" and "string" must have different instantiations, then you have to use some
other type constructor that is isomorphic to string, and do the instantiation for it.
Note that the type "String.literal" from theory String is such a copy, but I recommend
that you do not use this type copy for your purposes. String.literal has a specific
purpose for code generation, so if you ever want to generate code (especially in Haskell),
you will run into problems with String.literal.
Hope this helps,
On 25/02/15 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and