Stream: Beginner Questions

Topic: ✔ No code equation for pairs


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jakob Schulz (Dec 01 2022 at 21:30):

Ah, I see. Thank you very much! :)

view this post on Zulip Notification Bot (Dec 01 2022 at 21:30):

Jakob Schulz has marked this topic as resolved.


Last updated: Mar 29 2024 at 08:18 UTC