Dear Manuel,
I have not tried this explicitly, but it looks like the standard problem with type classes
in Scala (see section 7.1 in the code generator tutorial). Probably the problematic code
equations use two type classes with an operation inherited from the same anchestor. The
error message in the start of this thread hints at this problem. So you best introduce a
special type class for Scala (as has already been done for others in the code generator
tests).
Hope this helps,
Andreas
On 12/01/16 09:56, Manuel Eberl wrote:
I tried to trace this issue and I am really confused now.
The problem is apparently the following code equation I added for "binomial" at
the end of
Binomial.thy:
lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
If I delete this rule, everything works again. I then tried the following,
which also
produces the same error:
lemma binomial_code [code]:
"n choose k = (if k ≤ n then fact n div (fact k * fact (n - k)) else 0)"
The following two, on the other hand, work:
lemma binomial_code [code]:
"0 choose k = (if k = 0 then 1 else 0)"
"Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
lemma binomial_code [code]:
"n choose k = (if k = 0 then 1 else if n = 0 then 0 else ((n - 1) choose (k -
1)) + ((n -
1) choose k))"
So I thought maybe the "fact" is the problem, but the following works as well,
even though
it contains "fact":
lemma binomial_code [code]:
"n choose k =
(if k = 0 then 1 else if n = 0 ∧ fact n = fact n then 0 else ((n - 1)
choose (k -
1)) + ((n - 1) choose k))"
Does anybody have any idea what is going on here?
Manuel
_______________________________________________
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
