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

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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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