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"

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?


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