[isabelle-dev] Scala implicits

[Manuel Eberl]

The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used 
to break Codegenerator_Test. I can have a look later to see whether this 
is still the case.

If it is not, we should probably proceed to move some more of René 
Thiemann et al's efficient code equations from the AFP to the distribution.

I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:
> Dear power users of code generation to Scala,
>
> during the last months there have been some reports on ambiguity
> problems with implicits in Scala.
>
> One kind of these has been known for long and can be addressed in more
> recent versions of Scala, which has been done in 7cffe366d333.
>
> One other kind is presumably resolved with the patch attached,
> applicable to b3e5bdb784f5. The key idea is to generate implicits in
> Scala (stemming from type class instances) into the respective companion
> objects of corresponding type classes.
>
> Since I have no example at hand where such ambiguities have been
> observed to happen, I would kindly ask whether someone might try whether
> that patch resolves the issue. No problems on the visible theory
> universe (Isabelle distribution plus AFP) have been encountered.
>
> The patch still keeps the traditional Scala approach that each implicit
> dictionary holds all operations of all super classes. I don't know
> whether this is still apt to expose problems, but this could be tackled
> in a second step.
>
> Thanks to Lars Hupel for suggesting these solutions.
>
> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>