[isabelle-dev] Code generation in Isabelle

[Jasmin Christian Blanchette]

Am 18.10.2011 um 08:54 schrieb Lukas Bulwahn:

> Florian and I are not sure if code_inline or code_unfold fit better to the intended behaviour of "rewriting a code equation by some simplifying equation" (unfolding a term by its definition, or inlining the definition).

I would also vote for "code_unfold", if nothing else for consistency with the similar "nitpick_unfold" tag.

When I introduced "nitpick_unfold" I also considered "nitpick_inline", but concluded that the "unfold" terminology is from theorem proving and the "inline" terminology from the world of compilers. For the code generator, the argument swings both ways, though...

Jasmin