Re: [isabelle] type class instantiation



Hi Chris,

types ('f,'v)sub = "('v * ('f,'v)term)list"

Now I want to instantiate `sub' for the recpower class where the unit element is the empty substitution and multiplication is substitution composition. But already for

instantiation sub :: recpower begin

I get `Illegal type abbreviation: "Term.sub"'. What does that mean? Can I only instantiate types defined by `datatype'?

Only real type constructors can be instances of classes. Sub is just a type abbreviation. If you really need the instance, you must wrap up your substitutions in a real datatype.

Alex





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