Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions



Hi all,

> Please find attached:
> 
> * RealMinusBug.thy: a minimal example in which I tracked down the bug.
>  Please don't take the filename seriously; it's just that initially I
> thought the bug was related to real numbers.

I have identified the issue; it will not show up in the next Isabelle
release.

The issue occurs whenever there is a class parameter of type … => 'a,
and a corresponding dictionary is needed for a function type instance.
Maybe there is a chance to work around this in your application.  If
not, and there is pressure not to await the upcoming release, it would
be possible to provide the necessary adjustions as dedicated patches (we
do not do this often, but sometimes there is no directer way).

Cheers,
	Florian

-- 

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.