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
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44   E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet





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