# [isabelle] Problems with the Code-Generator

Dear all,

`I currently have the problem that the code-generator produces
``ambiguous function calls.
`
Consider the following theory:
theory Problem imports Rational Code_Char_chr
begin
fun f :: "rat ⇒ nat ⇒ bool"

`where "f x z = ((x * x = x) ∧ (if z = 3 then z = z div z else z =
``7))"
`
export_code f in Haskell file -

`Then one obtains code which cannot be compiled due to the following
``reason:
`
module Nat where {
...
data Nat = Zero_nat | Suc Nat.Nat;
divmod :: Nat.Nat -> Nat.Nat -> (Nat.Nat, Nat.Nat);
divmod m n = ...
}
module Integer where {
import Nat;
...
divmod :: Integer -> Integer -> (Integer, Integer);
divmod k l = ...
mod_int :: Integer -> Integer -> Integer;
mod_int a b = snd (divmod a b);
div_int :: Integer -> Integer -> Integer;
div_int a b = fst (divmod a b);
}

`Here, in the functions mod_int and div_int the call to divmod is
``ambiguous, it can refer to divmod within the Integer module or to
``divmod within the Nat module.
`
Is there any way how to avoid this situation?
Best regards,
Rene

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*