(Take the following with a grain of salt, it is the result of a cursory
investigation.)
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 =>
ROOT.semiring_char_0[ROOT.nat]
[error] and method semiring_div_nat in object ROOT of type =>
ROOT.semiring_div[ROOT.nat]
[error] match expected type ROOT.power[ROOT.nat]
[error] less_eq_nat(power[nat](m,
nat_of_integer(BigInt(2))),
[error] ^
The affected function is:
def sqrt(n: nat): nat =
Max[nat](filter[nat](((m: nat) =>
less_eq_nat(power[nat](m,
nat_of_integer(BigInt(2))),
n)),
seta[nat](upt(zero_nata, Suc(n)))))
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.
Cheers
Lars
* 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
disambiguate manually
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
