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)".

	Florian

-- 

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.