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,
	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.