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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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