[isabelle-dev] Explicit option "open" for code_reflect
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 15 11:36:02 CEST 2015
> Between Isabelle 2014 and 2015, the option "open" appeared for the
> command export_code, and by default the reflection minimizes the
> exported code.
> Would it be acceptable for code_reflect to also have a similar option
what is your use case? If you want to export an operation in the
generated code, just add it to the list of constants. It is the very
purpose of code_reflect to provide a well-defined interface.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev