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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
