Jakob Schulz (Dec 01 2022 at 21:16): Jakob Schulz (Dec 01 2022 at 21:16):Interesting. I am using Isabelle2022, and am working in a locale. Outside of the locale, there is no problem; but as soon as I am trying this in any locale, it doesn't work anymore. I edited the minimal working example.
Manuel Eberl (Dec 01 2022 at 21:18):Ah yes, code generation from inside locales is tricky because everything you define inside a locale, has the locale assumptions attached to its definition equation (and its simp equations in case of e.g. a function package function). The former is not strictly necessary, but the latter is, since function termination may be contingent on the locale assumptions.
Since the code generator can only work with unconditional code equations, this explains what you're seeing.
Jakob Schulz (Dec 01 2022 at 21:30):Ah, I see. Thank you very much! :)
Notification Bot (Dec 01 2022 at 21:30):Jakob Schulz has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC