Hi Fréderic, > 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 > "open"?
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.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
