[isabelle-dev] Code generation in Isabelle

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Oct 18 09:33:29 CEST 2011


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




More information about the isabelle-dev mailing list