Re: [isabelle] Integration of Scala code generated from Isabelle theories

Dear all Isabelle users,

Le 20/06/11 19:21, Florian Haftmann a écrit :
To get an idea how they should look, I recommend to have a look at
generated Scala code which contains implicit value definitions for class
instances, e.g.

	definition "foo = distinct [0, Suc 0]"

	export_code foo in Scala

If I understand well the generated code, to match my problem, I should simply write:

object Main {
  implicit def equal_nat: HOL.equal[String] = new HOL.equal[String] {
    val `HOL.equal` = (a: String, b: String) => a==b

  def main(args: Array[String]): Unit = {
    val l: List[String]= "John"::"Paul"::"George"::"Ringo"::Nil
    val b= testScala.member("John",l)


Instead of all the horrible implicit conversion of classes I wrote first :-)
This solution seems to be OK.
Thanks a lot Florian,

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.