Re: [isabelle] Scala generator

Hi all,

for a substantial solution I have to ask on the scala mailing list, this
will take some time.

Luckily there is a workaround for that: provide an explicit union of
both classes s.t. the resulting constraint only mentions one class:

class class3 = class1 + class2

lemma [code]:
  "(f :: 'a::class3) = elem"
  by (simp add: f_def)

Then it works fine.

Note that the preprocessor propagates sort constraints through systems
of code equations, so it might be enough to provide a more specialized
code lemma for exactly one operation.

Hope this helps in the first place,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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