Re: [isabelle] [code func] attribute on overloaded definitions
Thanks, Florian. But will this work for autoquickcheck? I thought
that used a separate code generator.
On May 13, 2008, at 2:38 AM, haftmann at mailbroy.informatik.tu-
indeed you can use the preprocessor to deal with overloading:
foo :: "'a => 'b => int"
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
Hope this helps
This archive was generated by a fusion of
Pipermail (Mailman edition) and