[isabelle-dev] Explicit option "open" for code_reflect

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 15 11:36:02 CEST 2015


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151015/eb7c408b/attachment.sig>


More information about the isabelle-dev mailing list