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

> 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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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