Re: [isabelle] Arity limitations of type classes?



Dear Rafal,

I have barely to add anything to Brian's excellent solution proposal
except that you should consider using Isabelle's class / instantiation
instead of the primitive axclass / instance.  A short tutorial can be
found at http://isabelle.in.tum.de/dist/Isabelle/doc/classes.pdf.

> Hopefully these type classes will work for you. However, I expect that
> defining overloaded operations on these type classes might be a bit
> tricky. Constant definitions would probably need to do case analysis on
> the cardinality of the type argument, but I haven't tried this.

Perhaps it is sufficent to provide a combinator like

definition bit_length_case :: "'b itself => 'a => 'a => 'a => 'a" where
  "bit_length_case TYPE('b) f g h = (if CARD('b) = 16 then f else if
CARD ('b) = 8 then g else ..."

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.