Re: [isabelle] Basic help with class and instantiation

Hi Yannick,

>>    instantiation int :: cls1
>>      begin
>>        definition df: "cls1_f n = f n"
>>        definition dg: "cls1_g n = g n"

without having really tried, I guess that the type of these definitions
is too general; try something like "cls1_f n = (f n :: int)".



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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