Re: [isabelle] Simple selective code generation?



Hi Thomas,

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?
With code_type?
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")

Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.