Re: [isabelle] Differences between code_reflect and export_code
In this example, I think they are the same. However, from my experience,
code_reflect is always used to make the code generation process static.
That is, when we are building a decision procedure based on
reflection/code generation, we really don't want the code generation
process to happen every time the decision procedure is called, instead
what we should expect is that the code is generated only once and
executed directly when needed. In this case, the file option is not used
In short, I believe code_reflect and export_code should be almost the
same with the file option, but in general they serve different purposes.
On 2015-03-24 15:57, Lars Hupel wrote:
Dear codegen experts,
what's the difference between
As far as I can tell, the effects are the same â SML code is being
produced and saved into a file, without processing it.
University of Cambridge
This archive was generated by a fusion of
Pipermail (Mailman edition) and