[isabelle-dev] HOL-Codegenerator_Test error
hupel at in.tum.de
Tue Jan 12 11:27:22 CET 2016
(Take the following with a grain of salt, it is the result of a cursory
As far as I can tell the current problem is a variation of §7.1.
Here's an excerpt from the error log:
[error] /tmp/foo/foo.scala:5687: ambiguous implicit values:
[error] both method semiring_char_0_nat in object ROOT of type =>
[error] and method semiring_div_nat in object ROOT of type =>
[error] match expected type ROOT.power[ROOT.nat]
The affected function is:
def sqrt(n: nat): nat =
Max[nat](filter[nat](((m: nat) =>
As can be seen, it is not parameterized over types. There are actually
two legitimate ambiguous implicit values (with the inherent ambiguity
stemming from the export scheme of instances to Scala*).
The solution here might very well be to "close the diamond", but I fail
to understand how this compiled in the first place.
* there is the possibility of improving the scheme to avoid the present
problem, but not the problem described in §7.1**
** if we want to fix §7.1 once and for all, the code generator needs to
More information about the isabelle-dev