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

Hi John,

indeed you can use the preprocessor to deal with overloading:

  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

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