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



Hello Andreas,

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.

Cheers
Lars




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