Re: [isabelle] type class instantiation

Hi Christian

> types ('f,'v)sub = "('v * ('f,'v)term)list"
> instantiation sub :: recpower begin
> I get `Illegal type abbreviation: "Term.sub"'.

"types" does only introduce a syntactic abbreviation, not a logical
type!  If you want to use type classes, you have to provide a separate
logical type, in the extreme case as a mere copy, e.g.:

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

primrec dest_Sub where "dest_Sub (Sub xs) = xs"

instantiation sub :: recpower begin


Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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