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
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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