[isabelle] [code func] attribute on overloaded definitions
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