Re: [isabelle] Simple selective code generation?

Dear all,

In my case it was also necessary to NOT re-generate the code for equality on the datatype (HOL.equal) and for some other given functions (here f). The function generated for equality on datatype toto is equal_toto so it is enough to use this identifier directly in the code_printing command (with a ' to quote the _)

To sum-up my code for Isabelle2014 is:
  type_constructor toto ⇀ (Scala) "toto"
  | constant M ⇀ (Scala) "M"
  | constant T ⇀ (Scala) "T"
  | constant f ⇀ (Scala) "f"
  | constant "HOL.equal :: toto ⇒ toto ⇒ bool" ⇀ (Scala) "equal'_toto"
And for Isabelle2012 it is:
code_abort f

code_type toto
  (Scala "toto")

code_const M
  (Scala "M")

code_const T
  (Scala "T")

code_const "HOL.equal ::"toto ⇒ toto ⇒ bool"
  (Scala "equal'_toto")

Best regards and thank you to Andreas!

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.