# [isabelle] [code func] attribute on overloaded definitions

Hi,
I am trying to generate executable code for some overloaded definitions:
consts cplus :: "'a => 'b => 'b"
defs (overloaded)
cplus_nat_int_def[code func]:
"cplus (a::nat) (b::int) == int a + b"
cplus_int_nat_def[code func]:
"cplus (a::int) (b::nat) == nat a + b"
However, the code generator gives the following error:
*** Type
*** nat => int => int
*** of defining equation
*** "cplus ?a ?b == int ?a + ?b"
*** is incompatible with declared function type
*** ?'a::type => ?'b::type => ?'b::type
*** At command "defs".

`What is the correct way to register code equations for overloaded
``functions?
`
Thanks,
-john

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