Re: [isabelle] Simple selective code generation?
code_printing type_constructor toto ⇀ (Scala) "Scratch.toto"
| constant M ⇀ (Scala) "Scratch.M"
| constant T ⇀ (Scala) "Scratch.T"
Bonus question: do you know how to perform this in Isabelle2012?
I don't have Isabelle2012 installed any more, but IIRC, the syntax was as follows:
code_type toto (Scala "Scratch.toto")
code_const M (Scala "Scratch.M")
code_const T (Scala "Scratch.T")
This archive was generated by a fusion of
Pipermail (Mailman edition) and