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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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