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

Hi John,
indeed you can use the preprocessor to deal with overloading:
consts
foo :: "'a => 'b => int"
defs (overloaded)
foo1_def: "foo (n::nat) (k::int) == int n - k"
foo2_def: "foo (k::int) (n::nat) == k + int n"
definition foo1 :: "nat => int => int" where
foo1_aux_def: "foo1 = foo"
definition foo2 :: "int => nat => int" where
foo2_aux_def: "foo2 = foo"
lemma [code func]:
"foo1 n k = int n - k"
"foo2 k n = k + int n"
unfolding foo1_aux_def foo2_aux_def foo1_def foo2_def by rule+
lemma [code inline]:
"foo = foo1"
"foo = foo2"
unfolding foo1_aux_def foo2_aux_def by rule+

`This will eliminate ad-hoc overloading before the code generator
``actually "sees" it. Note that this does *not* introduce any
``polymorphism due to overloading (for which you have to use type
``classes).
`
Hope this helps
Florian

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