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



Hi Thomas,

>   class StringWrapper(val s : String) extends HOL.equal[StringWrapper]{
>     def `HOL.equal`(s1:StringWrapper, s2:StringWrapper):Boolean = s1==s2
>   }
> 
> error: could not find implicit value for evidence parameter of type
> member.HOL.equal[String]
>   val b= testScala.member("John",l)

those implicit values must be values (val, def), not classes.

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

As I rule of thumb, I further recommend to avoid plumbing generated and
non-generated code as far as possible and doing as much as possible
within HOL.  Note that it is possible to generate Scala strings using
type String.literal with constructor STR:

	definition "foo = STR ''foo''"

	export_code foo in Scala

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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