Re: [isabelle] Simple selective code generation?

Le 11/09/14 10:19, Andreas Lochbihler a écrit :
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")

Yes, thanks to the explanation you gave me in your last e-mail + the List.thy file I just managed to get it right by myself.

Thanks a lot,

Best regards,

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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