Re: [isabelle] type class instantiation
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and