[isabelle] Simple selective code generation?
Dear all Isabelle users,
For our "formal software engineering" course (1), we use Isabelle/HOL to
generate Scala code to be integrated into bigger Scala developments.
One problem that we have is that when generating the code for a function
f ranging over a datatype T the code of the datatype is systematically
generated. Is it possible to filter out some types/functions for the
generation by export_code? and how?
We need this because, if the code for T is already present somewhere
else in the project, we have to manually edit the generated code.
Thanks in advance,
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and