Re: [isabelle] [code func] attribute on overloaded definitions
I suspect that the presence of two type variables in the generic type of
cplus is to blame. The code generator can only deal with overloading
that's resolved by a single type argument.
John Matthews schrieb:
I am trying to generate executable code for some overloaded definitions:
consts cplus :: "'a => 'b => 'b"
"cplus (a::nat) (b::int) == int a + b"
"cplus (a::int) (b::nat) == nat a + b"
However, the code generator gives the following error:
*** 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and