Re: [isabelle] [isabelle-dev] Code generation in Isabelle

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...


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