Re: [isabelle] Adding a code equation for a class parameter



>> many packages implicitly declare some code equations for the
>> constants you define. The code generator remembers that that these
>> declarations have been implicity, so when you explicitly declare a new
>> code equation, it silently drops the implicit ones. This behaviour is
>> sensible in many cases because the user otherwise would have to
>> manually delete the default equations first, which might not be that
>> easy. Therefore, you have to declare all the code equations you want.
> 
> thanks, that explanation makes perfect sense. I do wonder why there's no
> warning in this case, though, just like the warning you get when adding
> a code equation which subsumes others.

Since this would issue warnings in the common case that default code
equations stemming from definitions are replaced by elaborated code
equations.

	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.