[isabelle] type class instantiation
I have problems to instantiate the recpower class for parametric types.
E.g., I have defined substitutions as association lists from variables
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'? How do I write the
instantiation for parametric types (if possible at all)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and